Faster temporal reasoning for infinite-state programs
2014pp. 75–82
Citations Over TimeTop 13% of 2014 papers
Abstract
In this paper, we describe a new symbolic model checking procedure for CTL verification of infinite-state programs. Our procedure exploits the natural decomposition of the state space given by the control-flow graph in combination with the nesting of temporal operators to optimize reasoning performed during symbolic model checking. An experimental evaluation against competing tools demonstrates that our approach not only gains orders-of-magnitude performance improvement, but also allows for scalability of temporal reasoning for larger programs.
Related Papers
- → Algorithmic verification of linear temporal logic specifications(1998)131 cited
- → Reducing CTL-live Model Checking to First-Order Logic Validity Checking(2014)7 cited
- → Reducing CTL-live model checking to first-order logic validity checking(2014)5 cited
- Model Checking Using Partial Kripke Structure with 3-Valued Temporal Logic(2006)
- → Vectorized model checking for computation tree logic(2005)2 cited