Current trends in provable assertion derivation: Current trends in provable assertion derivation

Current trends in provable assertion derivation:

• Current trends in provable assertion derivation:

• An abstract framework is set up by the user
• The user must come up with a framework which is both expressive enough and sufficiently inexpensive
• Abstract domains
• Shapes and Templates
• Invariant templates
• Linear arithmetic
• Uninterrupted functions
• CEGAR
• The abstract interpretation refinement is done automatically
• But loops cause problem

Counterexamples can be seen as a full-fledge program

• Counterexamples can be seen as a full-fledge program

• A Path Program is not just a single infeasibility

• It can represent a whole family of them!

• So it is ideal for loops

• When we remove a path program, we are removing many false alarms

• Path program decomposes a large program into a set of smaller programs

• To achieve all these we must add universal quantifiers to the set!

We can overcome two limitations of CEGAR-based schemes

• We can overcome two limitations of CEGAR-based schemes

• Avoid iterative unwinding of loops
• We can treat infinite paths and also we can treat finite paths more efficiently

• We can handle a larger class of problems

• Dependence of correctness of program on arrays

What does BLAST do?

• What does BLAST do?

• No predicates are tracked and just reach ability checked

What does BLAST do?

• What does BLAST do?

• In the third phase it extracts the predicates and adds them to predicate abstraction

• But again for two iterations we need to do the same thing!

We infer path invariants from Path Programs

• We infer path invariants from Path Programs

• A path invariant map is a map from a location of the prog to a set of formulas

• Initial location maps to true
• For each (l, ρ,l’) in the path program, the successor of the formula at l with respect to the program operation ρ implies the formula at l’
• The path is safe, if the error location is mapped to formula false

A program is P=(X, L, l0, T, le)

• A program is P=(X, L, l0, T, le)

• Error location does not have any outgoing edges

• These together make a directed graph called the control-flow graph (CFG)

• A computation of the program is the sequence ,…,

• If (l, ρ,l’) is an edge in T then we have (si ,si+1) satisfies ρ

We use the template-based invariant generation

• We use the template-based invariant generation

• In template-based invariant synthesis, we assume that for each control location in the domain of the map η, we have a so-called invariant template, which is a parametric constraint over program variables.

We construct a suitable template by analyzing a given path program.

• We construct a suitable template by analyzing a given path program.

• If the program contains an assertion that is iteratively checked, then we add a universally quantified implication to the template.