BMC on Tuesday, August 15th

Competitions (09:00‑10:00)
Chair: Joćo Marques-Silva
Location: Metropolitan B

09:00‑09:20	Carsten Sinz SAT-Race Information on the SAT-Race remains on separate page.
09:20‑09:40	Olivier Roussel Pseudo Boolean Evaluation Information on the Pseudo Boolean Evaluation resides on a separate page.
09:40‑10:00	Armando Tacchella QBF Evaluation Information on the QBF Evaluation resides on a separate page.

Break (10:00‑10:30)

Session 2: Invited Talk (10:30‑11:30)

10:30‑11:30

Ilkka Niemela Bounded Model Checking, Answer Set Programming, and Fixed Points [pdf] Answer set programming (ASP) is a novel declarative paradigm for solving search problems. The basic idea of ASP is similar to, for example, SAT-based planning or constraint satisfaction problems but ASP has its roots in logic programming and the stable model semantics. ASP offers a powerful knowledge representation language for effective problem encoding supporting, for example, logical variables, recursive definitions, and a variety of aggregates. A number of successful ASP systems have already been developed and applied in areas such as planning, decision support for the flight controllers of space shuttles, web-based product configuration, configuration of a Linux distribution, VLSI routing, and linguistics. The talk explains the theoretical underpinnings of ASP, outlines computational techniques used in current ASP solvers, and then discusses bounded model checking (BMC) as a potential application area for ASP techniques. BMC can be seen as a search problem where the task is to find an execution of the system violating a given (temporal) property. ASP fit well such an application and offers promising techniques to encoding and solving BMC problems. In particular, ASP supports directly recursive fixed point computation needed to evaluate temporal operators and we discuss how this can be used in bounded model checking of linear temporal logic (LTL).

Session 3: Technical Papers (11:30‑12:30)

11:30‑12:00

Joao Marques-Silva (University of Southampton) Interpolant Learning and Reuse in SAT-Based Model Checking One of the most paradigmatic practical applications of Boolean Satisfiability (SAT) is bounded model checking (BMC). The utilization of SAT in model checking has allowed significant performance gains and, as a consequence, a large number of commercial verification tools now include SAT-based model checkers. Recent work has provided SAT-based BMC with completeness conditions, and this is generally referred to as unbounded model checking (UMC). Among the existing approaches for SAT-based UMC, the utilization of interpolants is among the most effective. Despite their success, interpolants have only been used for identifying a fixed point of the set of reachable states. This paper extends the utilization of interpolants in SAT-based model checking. This is achieved by observing that, under reasonable assumptions, interpolants can be {\em reused}, i.e. computed interpolants can be reused at later stages of the model checking process. The paper develops conditions for validity of interpolant reuse. Preliminary practical experience on interpolant learning and reuse is reported.

12:00‑12:30

Toni Jussila (Johannes Kepler University) Armin Biere (Johannes Kepler University) Compressing BMC Encodings with QBF Symbolic model checking is PSPACE complete. Since QBF is the standard PSPACE complete problem, it is most natural to encode symbolic model checking problems as QBF formulas and then use QBF decision procedures to solve them. We discuss alternative encodings for unbounded and bounded safety checking into SAT and QBF. One contribution is a linear encoding of simple path constraints, which usually are necessary to make k-induction complete. Our experimental results show that indeed a large reduction in the size of the generated formulas can be obtained. However, current QBF solvers seem not to be able to take advantage of these compact formulations. Despite these mostly negative results the availability of these benchmarks will help to improve the state-of-the-art of QBF solvers and make QBF based symbolic model checking a viable alternative.

Lunch break (12:30‑14:00)

Session 4: Invited Talk (14:00‑15:00)

14:00‑15:00

Fabio Somenzi Techniques for proving properties with SAT-based MC [pdf]

Session 5: Technical Paper (15:00‑15:30)

15:00‑15:30

Erika Abraham (Albert-Ludwigs-University Freiburg) Bernd Becker (Albert-Ludwigs-University Freiburg) Marc Herbstritt (Albert-Ludwigs-University Freiburg) Bounded Model Checking with Parametric Data Structures Bounded Model Checking (BMC) is a successful refutation method to detect errors in not only circuits and other binary systems but also in systems with more complex domains like timed automata or linear hybrid automata. Counterexamples of a fixed length are described by formulas in a decidable logic, and checked for satisfiability by a suitable solver. In an earlier paper we analyzed how BMC of linear hybrid automata can be accelerated already by appropriate encoding of counterexamples as formulas and by selective conflict learning. In this paper we introduce parametric datatypes for the internal solver structure that, taking advantage of the symmetry of BMC problems, remarkably reduce the memory requirements of the solver.

Break (15:30‑16:00)

Session 6: Technical Papers (16:00‑17:00)

16:00‑16:30

Xuandong Li (Nanjing University) Sumit Kumar Jha (Carnegie Mellon University) Lei Bu (Nanjing University) Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming The existing techniques for reachability analysis of linear hybrid automata do not scale well to problem sizes of practical interest. Instead of developing a tool to perform reachability check on all the paths of a linear hybrid automaton, a complementary approach is to develop an efficient path-oriented tool to check one path at a time where the length of the path being checked can be made very large and the size of the automaton can be made large enough to handle problems of practical interest. This approach of symbolic execution of paths can be used by design engineers to check important paths and thereby, increase the faith in the correctness of the system. Unlike simple testing, each path in our framework represents a dense set of possible trajectories of the system being analyzed. In this paper, we develop linear programming based techniques towards an efficient path-oriented tool for the bounded reachability analysis of linear hybrid systems.

16:30‑17:00

Paul Jackson (School of Informatics, University of Edinburgh) Daniel Sheridan (Adelard LLP) A compact linear translation for bounded model checking We present a syntactic scheme for translating future-time LTL bounded model checking problems into propositional satisfiability problems. The scheme is similar in principle to the Separated Normal Form encoding proposed in [5](Frisch, Sheridan, Walsh, FMCAD 2002) and extended to past time in [3](Cimatti, Roveri, Sheridan, FMCAD 2004): an initial phase involves putting LTL formulae into a normal form based on linear-time fixpoint characterisations of temporal operators. As with [3] and [6](Latvala,Biere, Heljanko,Junttila, FMCAD 2004), the size of propositional formulae produced is linear in the model checking bound, but the constant of proportionality appears to be lower. A denotational approach is taken in the presentation which is significantly more rigorous than that in [5] and [3], and which provides an elegant alternative way of viewing fixpoint based translations in [6] and [1](Biere, Cimatti, Clarke, Strichman, Zhu, Advances in Computers 58, 2003).