Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Last revision Both sides next revision | ||
sav07_lecture_14_skeleton [2007/05/03 10:59] vkuncak |
sav07_lecture_14_skeleton [2007/05/03 18:50] vkuncak |
||
---|---|---|---|
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 | ||
+ | * [[Galllier Logic Book]], Section 6.5 | ||