LARA

Constraint-based analysis

Key techniques:

  • postulate a linear template invariant
  • formulate standard condition for inductive invariant over templates
  • eliminate implication using Farkas lemma
  • remove existential quantifiers using quantifier elimination for real fields

Quantifier elimination does not scale in general. Some improvements:

  • parameteric linear assertion - special structure of the system
  • local and increasing consecution as approximations of exact strongest post (instantiate \mu multiplier with 0 or 1)
  • constraint simplification by substitution (rewriting)
  • factorization: transforms parameterized linear condition into a product, which becomes disjunction
  • additional lemmas

Counterexample-driven analysis

Loop invariants in demand

Counterexample Driven Refinement for Abstract Interpretation

Key points:

  • abstract interepretation
  • automated refinement of domain
    • compare to ASTREE (also some parameters, e.g. packing)
    • refinement of when to widen and merge
  • how to check if counterexample is real
  • notion of powerdomain
  • widening for powerdomains
  • non-monotonicity of widening
  • experimental evaluation with proving given invariants