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

tarix  17.11.2018  ölçüsü  0,61 Mb.   #80061 

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
 Invariant templates
 CEGAR
 The abstract interpretation refinement is done automatically
 But loops cause problem
Counterexamples can be seen as a fullfledge program Counterexamples can be seen as a fullfledge program 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 To achieve all these we must add universal quantifiers to the set!
We can overcome two limitations of CEGARbased schemes We can overcome two limitations of CEGARbased schemes 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? 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 controlflow graph (CFG) A computation of the program is the sequence ,…,
We use the templatebased invariant generation We use the templatebased invariant generation In templatebased invariant synthesis, we assume that for each control location in the domain of the map η, we have a socalled 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.
Dostları ilə paylaş: 

