Inproceedings3978332197: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Clemens |ErsterAutorNachname=Dubslaff |FurtherAuthors=Patrick Wienhöft; Ansgar Fehnker}} {{Inproceedings |Title=Be lazy and don’t care: Faster CTL model checking for recursive state machines |Editor=Radu Calinescu and Corina S. Păsăreanu |Year=2021 |Booktitle=Software Engineering and Formal Methods |Volume=13085 |Pages=332–350 |Publisher=Springer |Series=Lecture Notes in Computer Science }…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
| Zeile 16: | Zeile 16: | ||
|DOI Name=10.1007/978-3-030-92124-8_19 | |DOI Name=10.1007/978-3-030-92124-8_19 | ||
|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 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. | |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 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= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} | ||
Aktuelle Version vom 5. März 2025, 15:42 Uhr
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
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
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
- 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: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@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}
}
