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

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

• Use large block encoding to improve performance (LargeBlockEncodingIcfgTransformer, mApplyLargeBlockEncoding)

• Use live variables to optimize size of templates (generateLiveVariables, USE_LIVE_VARIABLES)

• We use classes that implement the IPredicate interface to represent sets of states

• Different strategies to increase size of templates. (maybe we can use the same classes and interfaces, maybe not ILinearInequalityInvariantPatternStrategy)

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
• we do not use unsatisfiable cores while synthesizing danger invariants
• we do not use over/underapproximations of reachable states to guide constrution of templates ( loc2underApprox loc2overApprox)
• We have Skolem function
• Code of safety invariant synthesis is probably not well-structures and only partly documented. The code for danger invariant should be fully documented
• For the synthesis of safety invariants we do not have to synthesize annotation for the initial location(s), we can use the preconditions. (Same does not hold for danger invariants)

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?
• Generalize LinearInequalityInvariantPatternProcessor
  1. Change hardcoded init and error annotation
  2. Allow multiple init locations and error locations (not important)
  3. Make synthesis of invariant for initial location(s) optional