Decision Procedures for Second Order Logic

Program analysis and verification problems can be stated as formulae in certain fragments of second order logic. Solutions to such formulae are predicates that satisfy existential or optimisation conditions defined by the problem to solve. Since solving these formulae exactly is often infeasible (due to undecidability or intractability), we aim at finding approximate solutions with well-defined guarantees. Abstract interpretation is a framework for approximately solving program analysis problems with such guarantees. Decision procedures are algorithms typically used in SAT and SMT solvers to solve propositional and first-order logical formulae. Our goal is to combine both techniques in order to build second-order logic solvers targeted at program analysis and verification problems.

  • Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Björn Wachter. Synthesising Interprocedural Bit-Precise Termination Proofs. In Automated Software Engineering, ASE'15, pp. 53-64, IEEE, 2015. [bibtex] [link] [website]
  • Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel. Safety Verification and Refutation by k-Invariants and k-Induction. In Static Analysis, SAS'15, Vol. 9291 of LNCS, pp. 145-161, Springer, 2015. [bibtex] [link] [website]
  • Martin Brain, Cristina David, Daniel Kroening, Peter Schrammel. Model and Proof Generation for Heap-Manipulating Programs. In Programming Languages and Systems, ESOP'14, Vol. 8410 of LNCS, pp. 432-452, Springer, 2014. [bibtex] [link]


Research Interests