DiVer: SAT-based model checking platform for verifying large scale systems. 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.
Keywords for this software
References in zbMATH (referenced in 10 articles , 1 standard article )
Showing results 1 to 10 of 10.
- Jayalalitha, G.; Uthayakumar, R.: Fractal approach to understand PFO and DCS in sport divers (2010)
- Cecil, Matthew: The Ricci curvature of finite dimensional approximations to loop and path groups (2009)
- Schlich, Bastian; Kowalewski, Stefan: Model checking C source code for embedded systems (2009)
- Ivančić, Franjo; Yang, Zijiang; Ganai, Malay K.; Gupta, Aarti; Ashar, Pranav: Efficient SAT-based bounded model checking for software verification (2008)
- Ganai, Malay; Gupta, Aarti: SAT-based scalable formal verification solutions (2007)
- Collavizza, Hélène; Rueher, Michel: Exploration of the capabilities of constraint programming for software verification (2006)
- Gupta, Aarti; Ganai, Malay K.; Wang, Chao: SAT-based verification methods and applications in hardware verification (2006)
- Gupta, A.K.; Kasturiratna, D.; Nguyen, T.; Pardo, L.: A new family of BAN estimators for polytomous logistic regression models based on $\varphi$-divergence measures (2006)
- Ganai, Malay K.; Gupta, Aarti; Ashar, Pranav: DiVer: SAT-based model checking platform for verifying large scale systems (2005)
- Ivančić, F.; Yang, Z.; Ganai, M.K.; Gupta, A.; Shlyakhter, I.; Ashar, P.: F-Soft: Software verification platform (2005)