This page is a demo of CTL Model Checking Algorithm for Self-Modifying Dynamic Pushdown Networks. If you want to know about SM-DPNs, please look at the LTL model checking paper:

• Touili, Tayssir, and Olzhas Zhangeldinov. “LTL Model Checking of Concurrent Self Modifying Code.” In Proceedings: The 29th International Conference on Engineering of Complex Computer Systems (ICECCS 2025). Full Paper