Programming Z3
(2022) : Nikolaj Bj{\o}rner and Leonardo de Moura and Lev Nachmanson and and Christoph Wintersteiger
url:
https://theory.stanford.edu/~nikolaj/programmingz3.html#SMT #bounded_model_checking #programming #python #reference #z3#my_bibtexBounded reachability of model programs - Microsoft Research
Model programs represent labeled transition systems and are used to specify expected behavior of systems at a high level of abstraction. Such programs are common as high-level executable specifications of complex protocols. Model programs typically use abstract data types such as sets and maps, and comprehensions to express complex state updates. Such models are mainly […]
Symbolic model checking using SAT procedures instead of BDDs
(1999) : A. Biere and A. Cimatti and E.M. Clarke and M. Fujita and Y. Zhu
DOI:
https://doi.org/10.1109/dac.1999.781333#FSMs #SAT #bounded_model_checking #model_checking#my_bibtex
Symbolic model checking using SAT procedures instead of BDDs
In this paper, we study the application of propositional decision procedures in hardware verification. In particular, we apply bounded model checking to equivalence and invariant checking. We present several optimizations that reduce the size of generated propositional formulas. In many instances, our SAT-based approach can significantly outperform BDD-based approaches. We observe that SAT-based techniques are particularly efficient in detecting errors in both combinational and sequential designs.
Symbolic Model Checking without BDDs
(1999) : Armin Biere and Alessandro Cimatti and Edmund Clarke and Yunshan Zhu
DOI:
https://doi.org/10.1007/3-540-49059-0_14#transition_system #SAT #bounded_model_checking #model_checking#my_bibtex
nope