 |
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 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]
|
|
|
 |
Peter
Schrammel
|
|
|
|
|
|
|
|
|
|
|
|
