A implementation of roperty-directed reachability (PDR) algorithm [1] based on Z3 SMT solver.
- Python 3.5.1.
- z3py: Z3 SMT solver with Python binding.
python ./pdr/test.py
[1] Een, Niklas, Alan Mishchenko, and Robert Brayton. "Efficient implementation of property directed reachability." Formal Methods in Computer-Aided Design (FMCAD), 2011. IEEE, 2011.