Bounded Model Checking with Parametric Data Structures

9 years 3 months ago
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. Key words: BMC, Hybrid Automata, Parametric Data Structures, SAT.
Erika Ábrahám, Marc Herbstritt, Bern
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Authors Erika Ábrahám, Marc Herbstritt, Bernd Becker, Martin Steffen
Comments (0)