Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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