MIND
Subproject |
S1 |
Categories |
Systems of systems / blackbox tools |
Overview |
MIND is a symbolic CTL model checker for partial designs based on BDDs or AIGs as an internal data structure. MIND implements various approximate and exact methods providing sound results on realizability and validity of CTL formulas for partial designs. Moreover, MIND is able to compute "uniform counterexamples" which are valid for all possible blackbox implementations. If approximate methods are not able to prove non-realizability or validity of CTL formulas, then blackboxes may be enhanced by requirements specifying their expected behaviour (leading to "grey Boxes"). MIND automatically selects subsets of these requirements which are needed to complete the proof. |
T. Nopper, C. Miller, M. Lewis, B. Becker, and C. Scholl. SAT Modulo BDD - A Combined Verification Approach for Incomplete Designs. In GI/ITG/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", 2010. C. Miller, T. Nopper, and C. Scholl. Symbolic CTL model checking for incomplete designs by selecting property-specific subsets of local component assumptions. In GI/ITG/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", 2009. T. Nopper und C. Scholl. Counterexample Generation for Incomplete Designs. In GI/ITG/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", 2007. T. Nopper und C. Scholl. Flexible Modeling of Unknowns in Symbolic Model Checking for Incomplete Designs. In GI/ITG/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", 2005. T. Nopper und C. Scholl. Approximate Symbolic Model Checking for Incomplete Designs. In Formal Methods in Computer-Aided Design, pages 290-305, 2004. T. Nopper und C. Scholl. Approximate Symbolic Model Checking for Incomplete Designs. In International Workshop on Logic and Synthesis, pages 377-384, Jun 2004. |
|
Pipelined ALU, VLIW-Alu, FFB, VIS Benchmarks |
|
Download |
Click here for binary & manual. |
Manual |
(see above) |
Status |
Prototype |