Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav07_lecture_14_skeleton [2007/05/03 10:59] vkuncak |
sav07_lecture_14_skeleton [2007/05/03 19:03] 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]] | ||
| Line 32: | Line 32: | ||
| * [[http://www.cs.wisc.edu/wpis/papers/tr1386.pdf|Program analysis via graph reachability]] | * [[http://www.cs.wisc.edu/wpis/papers/tr1386.pdf|Program analysis via graph reachability]] | ||
| * [[http://doi.acm.org/10.1145/379605.379690|Bebop: a path-sensitive interprocedural dataflow engine, Thomas Ball, Sriram K. Rajamani. PASTE 2001: 97-103]] | * [[http://doi.acm.org/10.1145/379605.379690|Bebop: a path-sensitive interprocedural dataflow engine, Thomas Ball, Sriram K. Rajamani. PASTE 2001: 97-103]] | ||
| + | |||
| ==== Counterexample-driven refinement ==== | ==== Counterexample-driven refinement ==== | ||
| Line 44: | Line 45: | ||
| Craig's interpolation theorem | Craig's interpolation theorem | ||
| + | * [[Gallier Logic Book]], Section 6.5 | ||
| + | * [[http://www.kenmcmil.com/pubs/TACAS04.pdf|An Interpolating Theorem Prover]] | ||
| + | [[http://www.kenmcmil.com/pubs/CAV06.pdf|Lazy Abstraction with Interpolants]] | ||