Lazy model checking for recursive state machines

Research output: Contribution to journalResearch articleContributedpeer-review

Abstract

Recursive state machines (RSMs) are state-based models for procedural programs with wide-ranging applications in program verification and interprocedural analysis. Model-checking algorithms for RSMs and related formalisms have been intensively studied in the literature. In this article, we devise a new model-checking algorithm for RSMs and requirements in computation tree logic (CTL) that exploits the compositional structure of RSMs by ternary model checking in combination with a lazy evaluation scheme. Specifically, a procedural component is only analyzed in those cases in which it might influence the satisfaction of the CTL requirement. We implemented our model-checking algorithms and evaluate them on randomized scalability benchmarks and on an interprocedural data-flow analysis of Java programs, showing both practical applicability and significant speedups in comparison to state-of-the-art model-checking tools for procedural programs.

Details

Original languageEnglish
Pages (from-to)369-401
Number of pages33
JournalSoftware and systems modeling
Volume23
Issue number2
Publication statusPublished - 20 Mar 2024
Peer-reviewedYes

External IDs

Scopus 85188171011
Mendeley fc9e6c12-b51f-3876-8ddd-f2d9f6b12cc9

Keywords

DFG Classification of Subject Areas according to Review Boards

Subject groups, research areas, subject areas according to Destatis

Keywords

  • Interprocedural static analysis, Model checking, Computation tree logic, Lazy verification, Recursive state machines