LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav07_lecture_12_skeleton [2007/04/26 13:19]
vkuncak
sav07_lecture_12_skeleton [2007/04/26 13:43]
vkuncak
Line 18: Line 18:
  
 ===== Counterexample-driven analysis ===== ===== Counterexample-driven analysis =====
 +
 +==== Loop invariants in demand ====
  
   * Paper: [[http://​research.microsoft.com/​~leino/​papers/​krml155.pdf|Loop invariants on demand]]   * Paper: [[http://​research.microsoft.com/​~leino/​papers/​krml155.pdf|Loop invariants on demand]]
  
- +==== Counterexample Driven Refinement for Abstract Interpretation ​====
-==== Loop invariants in demand ​====+
  
   * Paper: [[http://​research.microsoft.com/​copyright/​accept.asp?​path=http://​research.microsoft.com/​~sriram/​Papers/​tacas2006.pdf&​amp;​pub=15%22|Counterexample Driven Refinement for Abstract Interpretation]]   * Paper: [[http://​research.microsoft.com/​copyright/​accept.asp?​path=http://​research.microsoft.com/​~sriram/​Papers/​tacas2006.pdf&​amp;​pub=15%22|Counterexample Driven Refinement for Abstract Interpretation]]
Line 30: Line 31:
   * automated refinement of domain   * automated refinement of domain
      * compare to ASTREE (also some parameters, e.g. packing)      * compare to ASTREE (also some parameters, e.g. packing)
-     * refinement of when to widen +     * refinement of when to widen and merge 
-     ​* widening ​over powerset domain+  how to check if counterexample is real 
 +  * widening on abstract  
 +  * non-monotonicity of widening
   * experimental evaluation with proving given invariants   * experimental evaluation with proving given invariants
 +
  
 ==== Predicate abstraction ==== ==== Predicate abstraction ====