Skip to content

PolyhedralDangerInvariants

Matthias Heizmann edited this page Jul 17, 2017 · 27 revisions

Polyhedral Danger Invariants

High level comparison of danger invariants and safety invariants implementation

Commonalities

  • 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.

Differences

  • 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

Tasks

  • 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?
Clone this wiki locally