About

There are many books on the theory of model checking, but few on its implementation. While there are open-source model checkers available, they tend to be large and complex. The purpose of this project is to provide a "hackable" implementation of a model checker for learners.

References

• Bryant, "Graph-Based Algorithms for Boolean Function Manipulation" in IEEE Transactions on Computers, vol. C-35, no. 8, pp. 677-691, Aug. 1986, doi: 10.1109/TC.1986.1676819.
• Clarke, E. M., Jr, Grumberg, O., Kroening, D., Peled, D., & Veith, H. (2018). Model Checking, Second Edition. MIT Press.
• チェシャ猫 (2024). モデル検査器をつくる