LARA Some predicate abstraction papers: Construction of abstract state graphs with PVS Boolean and Cartesian Abstraction for Model Checking C Programs, Thomas Ball, Andreas Podelski, Sriram K. Rajamani. TACAS 2001: 268-283 (paper in .PS format) Automatic Predicate Abstraction of C Programs, Thomas Ball, Rupak Majumdar, Todd D. Millstein, Sriram K. Rajamani. PLDI 2001: 203-213 Bebop: a path-sensitive interprocedural dataflow engine, Thomas Ball, Sriram K. Rajamani. PASTE 2001: 97-103 Predicate abstraction for software verification Lazy abstraction Asbtractions from proofs