-
Notifications
You must be signed in to change notification settings - Fork 41
PolyhedralDangerInvariants
Matthias Heizmann edited this page Jul 17, 2017
·
27 revisions
-
Input is ICFG (interprocedural control flow graph)
-
We map templates to locations of program
-
Calls and Returns are not yet supported. We use our Boogie procedure inlining to handle programs with several procedures (hence, we cannot handle recursive programs).
-
Polyhedra-based (both use Boolean combinations of linear inequalities) Need translation of transition relation into linear inequalities.
-
Apply Motzkin transformation to constraints in order to reduce non-linear arithmetic and to get rid of quantifier alternation
-
Use SMT solver to get satisfying assignments for contraints. Apply simplification to obtain simple solution.
-
We start with small templates and iteratiable increase the size of the template.
- Synthesis of safety invariants also works with overapproximations of transition relation.
- We can check correctness of a safety invariant (by checking Hoare triples)
- safety invariants: error locations annotated with false, danger invariants: error locations annotated with true
- Translation of transition relation into linear inequalities: check if we can detect overapproximations.
- How can we check correctness of a danger invariant (warning: do not implement this, something similar might have been already implemented in Ultimate)?
- Which statistical data is interesting for our synthesis of danger invariants?
- Home
- Ultimate Development
- Ultimate Build System
- Documentation
- Project Topics