„03“ befindet sich nicht in der Liste (Januar, Februar, März, April, Mai, Juni, Juli, August, September, Oktober, ...) zulässiger Werte für das Attribut „Month“.

Lazy model checking for recursive state machines

Clemens DubslaffClemens Dubslaff, Patrick WienhöftPatrick Wienhöft, Ansgar FehnkerAnsgar Fehnker

DOI Link

Clemens Dubslaff, Patrick Wienhöft, Ansgar Fehnker
Lazy model checking for recursive state machines
Software and Systems Modeling, 1-33, 2024

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{DWF2024,
  author  = {Clemens Dubslaff and Patrick Wienh{\"{o}}ft and Ansgar Fehnker},
  title   = {Lazy model checking for recursive state machines},
  journal = {Software and Systems Modeling},
  year    = {2024},
  pages   = {1-33},
  doi     = {10.1007/s10270-024-01159-z}
}