Input-Based Three-Valued Abstraction Refinement

Autoři: Jan Onderka
doc. Dipl. Ing. Stefan Ratschan, Dr. tech.
Rok vydání: 2026
Typ publikace: Konferenční příspěvek (mezinárodní konf.)
Periodikum: Verification, Model Checking, and Abstract Interpretation. VMCAI 2026 Proceedings
Bibliografická citace: ONDERKA, Jan, RATSCHAN, Stefan. Input-Based Three-Valued Abstraction Refinement. In: CHEN, Y.-F., JENSEN, T., LENGÁL, O., eds. Verification, Model Checking, and Abstract Interpretation. VMCAI 2026 Proceedings. Cham: Springer, 2026, S. 237-262. Lecture Notes in Computer Science, 16417. ISBN 978-3-032-15699-0. ISSN 0302-9743
Dostupné z: doi:10.1007/978-3-032-15700-3_12.
DOI: 10.1007/978-3-032-15700-3_12
ID: 649281
Online záznam: Zobrazit online záznam

Abstrakt

Unlike Counterexample-Guided Abstraction Refinement (CEGAR), Three-Valued Abstraction Refinement (TVAR) is able to verify all properties of the μ -calculus. We present a novel algorithmic framework for TVAR that employs a simulator-like approach to build and refine the abstract state space with input-based splitting. This leads to a state space formalism that is much simpler than in previous TVAR frameworks, which use modal transitions. We implemented the framework in our open-source tool machine-check and verified properties of machine-code systems for the AVR architecture, showing the ability to verify systems and μ -calculus properties not verifiable by naïve model checking or CEGAR, respectively. This is the first practical use of TVAR for machine-code verification.