Be lazy and don’t care: Faster CTL 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
Be lazy and don’t care: Faster CTL model checking for recursive state machines
In Radu Calinescu and Corina S. Păsăreanu, eds., Software Engineering and Formal Methods, volume 13085 of Lecture Notes in Computer Science, 332–350, 2021. Springer

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 and various temporal logic specifications have been intensively studied in the literature. In this paper, 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 evaluate our prototypical implementation 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: Verifikation und formale quantitative Analyse„Verifikation und formale quantitative Analyse“ befindet sich nicht in der Liste (Computational Logic, Automatentheorie, Wissensverarbeitung, Knowledge-Based Systems, Knowledge Systems, Wissensbasierte Systeme, Logische Programmierung und Argumentation, Algebra und Diskrete Strukturen, Knowledge-aware Artificial Intelligence, Algebraische und logische Grundlagen der Informatik) zulässiger Werte für das Attribut „Forschungsgruppe“.Algebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-030-92124-8_19.

@inproceedings{DWF2021,
  author    = {Clemens Dubslaff and Patrick Wienh{\"{o}}ft and Ansgar Fehnker},
  title     = {Be lazy and don’t care: Faster {CTL} model checking for
               recursive state machines},
  editor    = {Radu Calinescu and Corina S. P{\u{a}}s{\u{a}}reanu},
  booktitle = {Software Engineering and Formal Methods},
  series    = {Lecture Notes in Computer Science},
  volume    = {13085},
  publisher = {Springer},
  year      = {2021},
  pages     = {332{\textendash}350},
  doi       = {10.1007/978-3-030-92124-8_19}
}