Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
predicate_abstraction [2007/03/31 18:22] lvariu |
predicate_abstraction [2007/05/02 09:44] vkuncak |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| Some predicate abstraction papers: | Some predicate abstraction papers: | ||
| - | * Boolean and Cartesian Abstraction for Model Checking C Programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani. TACAS 2001: 268-283 | + | * [[http://www-verimag.imag.fr/~graf/biblio.php?view=full#GrafSaidi97|Construction of abstract state graphs with PVS]] |
| + | * [[http://www.mpi-sb.mpg.de/~podelski/papers/cartesian.ps|Boolean and Cartesian Abstraction for Model Checking C Programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani. TACAS 2001: 268-283 (paper in .PS format)]] | ||
| * [[http://doi.acm.org/10.1145/378795.378846|Automatic Predicate Abstraction of C Programs, Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani. PLDI 2001: 203-213]] | * [[http://doi.acm.org/10.1145/378795.378846|Automatic Predicate Abstraction of C Programs, Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani. PLDI 2001: 203-213]] | ||
| * [[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]] | ||