Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines

Clemens Dubslaff*, Patrick Wienhöft, Ansgar Fehnker

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Downloads (Pure)

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 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 analysed 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.
Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods
Subtitle of host publication19th International Conference
PublisherSpringer
Publication statusAccepted/In press - 6 Dec 2021
Event19th International Conference on Software Engineering and Formal Methods, SEFM 2021 - Virtual Conference
Duration: 6 Dec 202110 Dec 2021
Conference number: 19

Conference

Conference19th International Conference on Software Engineering and Formal Methods, SEFM 2021
Abbreviated titleSEFM 2021
CityVirtual Conference
Period6/12/2110/12/21

Keywords

  • Model Checking
  • recursive state machines
  • Lazy Evaluation

Fingerprint

Dive into the research topics of 'Be Lazy and Don't Care: Faster CTL Model Checking for Recursive State Machines'. Together they form a unique fingerprint.

Cite this