Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav07_lecture_12_skeleton [2007/04/26 13:32]
vkuncak
sav07_lecture_12_skeleton [2007/04/26 13:43] (current)
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 ====
 +
 +  * 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]]
  
 Key points: Key points:
Line 31: Line 37:
   * experimental evaluation with proving given invariants   * experimental evaluation with proving given invariants
  
- 
-==== 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]] 
  
 ==== Predicate abstraction ==== ==== Predicate abstraction ====
 
sav07_lecture_12_skeleton.txt · Last modified: 2007/04/26 13:43 by vkuncak
 
© EPFL 2018 - Legal notice