DiVer: SAT-based model checking platform for verifying large scale systems

Malay K. Ganai, Aarti Gupta, Pranav Ashar

Research output: Contribution to journalConference article

9 Scopus citations

Abstract

We present a SAT-based model checking platform (DiVer) based on robust and scalable algorithms that are tightly integrated for verifying large scale industry designs. DiVer 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. DiVer 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.

Original languageEnglish (US)
Pages (from-to)575-580
Number of pages6
JournalLECTURE NOTES IN COMPUTER SCIENCE
Volume3440
DOIs
StatePublished - 2005
Externally publishedYes
Event11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 - Edinburgh, United Kingdom
Duration: Apr 4 2005Apr 8 2005

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'DiVer: SAT-based model checking platform for verifying large scale systems'. Together they form a unique fingerprint.

  • Cite this