Catálogo de publicaciones - libros

We present a SAT-based model checking platform () based on robust and scalable algorithms that are tightly integrated for verifying large scale industry designs. houses various SAT-based engines each targeting capacity and performance issues inherent in verifying large designs. The engines with their respective roles are as follows: Bounded Model Checking (BMC) and Distributed BMC over a network of workstations for falsification, Proof-based Iterative Abstraction (PBIA) for model reduction, SAT-based Unbounded Model Checking and Induction for proofs, Efficient Memory Modeling (EMM) and its combination with PBIA in BMC for verifying embedded memory systems with multiple memories (with multiple ports and arbitrary initial state). Using several industrial case studies, we describe the interplay of these engines highlighting their contribution at each step of verification. has matured over 3 years and is being used extensively in several industry settings. Due to an efficient and flexible infrastructure, it provides a very productive verification environment for research and development.

The equivalence checking problem consists in verifying that a system (e.g., a ) matches its abstract specification (e.g., a ) by comparing their Labeled Transition Systems (s) modulo a given equivalence relation. Two approaches are traditionally used to perform equivalence checking: verification requires to construct the two s before comparison, whereas (or ) verification allows to explore them incrementally during comparison. The latter approach is able to detect errors even in prohibitively large systems, and therefore reveals more effective in combating state explosion.