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 Both sides next revision
sav07_lecture_14_skeleton [2007/05/03 10:59]
vkuncak
sav07_lecture_14_skeleton [2007/05/03 10:59]
vkuncak
Line 17: Line 17:
 Readings: Readings:
   * [[http://​www.cs.cmu.edu/​~bryant/​pubdir/​ieeetc86.pdf|Graph-based algorithms for boolean function manipulation]]   * [[http://​www.cs.cmu.edu/​~bryant/​pubdir/​ieeetc86.pdf|Graph-based algorithms for boolean function manipulation]]
 +  * [[http://​citeseer.ist.psu.edu/​burch90symbolic.html|Symbolic Model Checking: 10^20 States and Beyond]]
   * [[http://​www.kenmcmil.com/​thesis.html|Ken McMillan'​s thesis]]   * [[http://​www.kenmcmil.com/​thesis.html|Ken McMillan'​s thesis]]
   * [[http://​nusmv.irst.itc.it/​index.html|NuSMV]]   * [[http://​nusmv.irst.itc.it/​index.html|NuSMV]]
Line 22: Line 23:
 ==== Checking for finite diameter systems ==== ==== Checking for finite diameter systems ====
  
-  * [[http://​citeseer.ist.psu.edu/​burch90symbolic.html|Symbolic Model Checking: 10^20 States and Beyond]] 
   * [[http://​www.springerlink.com/​content/​ahvlxugl1d7xrt28/​|Interpolation and SAT-Based Model Checking]]   * [[http://​www.springerlink.com/​content/​ahvlxugl1d7xrt28/​|Interpolation and SAT-Based Model Checking]]
   * [[http://​www.cs.cmu.edu/​~emc/​papers/​Conference%20Papers/​Completeness%20and%20complexity.pdf|Completeness and complexity of bounded model checking]]   * [[http://​www.cs.cmu.edu/​~emc/​papers/​Conference%20Papers/​Completeness%20and%20complexity.pdf|Completeness and complexity of bounded model checking]]