PolyhedralDangerInvariants

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

Differences

• Synthesis of safety invariants also works with overapproximations of transition relation.

Tasks

• Translation of transition relation into linear inequalities: check if we can detect overapproximations.