Selected Papers of the Conference ''Computer Aided Verification 2005''

2005

Editors: Kousha Etessami, Sriram K. Rajamani


1. Linear Encodings of Bounded LTL Model Checking

Biere, Armin ; Heljanko, Keijo ; Junttila, Tommi ; Latvala, Timo ; Schuppan, Viktor.
We consider the problem of bounded model checking (BMC) for linear temporal logic (LTL). We present several efficient encodings that have size linear in the bound. Furthermore, we show how the encodings can be extended to LTL with past operators (PLTL). The generalised encoding is still of linear […]

2. Predicate Abstraction with Under-approximation Refinement

Pasareanu, Corina S. ; Pelanek, Radek ; Visser, Willem.
We propose an abstraction-based model checking method which relies on refinement of an under-approximation of the feasible behaviors of the system under analysis. The method preserves errors to safety properties, since all analyzed behaviors are feasible by definition. The method does not require […]

3. Predicate Abstraction via Symbolic Decision Procedures

Lahiri, Shuvendu K. ; Ball, Thomas ; Cook, Byron.
We present a new approach for performing predicate abstraction based on symbolic decision procedures. Intuitively, a symbolic decision procedure for a theory takes a set of predicates in the theory and symbolically executes a decision procedure on all the subsets over the set of predicates. The […]

4. Interpolant-Based Transition Relation Approximation

Jhala, Ranjit ; McMillan, Kenneth L..
In predicate abstraction, exact image computation is problematic, requiring in the worst case an exponential number of calls to a decision procedure. For this reason, software model checkers typically use a weak approximation of the image. This can result in a failure to prove a property, even given […]