
Research



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 welldefined
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 firstorder logical formulae.
Our goal is to combine both techniques in order to build
secondorder logic solvers targeted at program analysis and
verification problems.
 HongYi Chen, Cristina David, Daniel Kroening, Peter Schrammel,
Björn Wachter. Synthesising Interprocedural BitPrecise
Termination Proofs. In Automated Software Engineering, ASE'15, pp. 5364, IEEE, 2015.
[bibtex]
[link]
[website]
 Martin Brain, Saurabh Joshi, Daniel Kroening, Peter Schrammel. Safety Verification and Refutation by kInvariants and kInduction. In Static Analysis, SAS'15, Vol. 9291 of LNCS, pp. 145161, Springer, 2015.
[bibtex]
[link]
[website]
 Martin Brain, Cristina David, Daniel Kroening, Peter Schrammel.
Model and Proof Generation for HeapManipulating Programs. In
Programming Languages and Systems, ESOP'14, Vol. 8410 of LNCS, pp. 432452, Springer, 2014.
[bibtex]
[link]




Peter Schrammel







