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



Yüklə 452 b.
tarix17.11.2018
ölçüsü452 b.



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

  • 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 control-flow graph (CFG)

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



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.




Dostları ilə paylaş:


Verilənlər bazası müəlliflik hüququ ilə müdafiə olunur ©genderi.org 2017
rəhbərliyinə müraciət

    Ana səhifə