Sie befinden Sich nicht im Netzwerk der Universität Paderborn. Der Zugriff auf elektronische Ressourcen ist gegebenenfalls nur via VPN oder Shibboleth (DFN-AAI) möglich. mehr Informationen...
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
Ist Teil von
Formal methods in system design, 2023-10
Erscheinungsjahr
2023
Link zum Volltext
Quelle
2022 ECC(Springer)
Beschreibungen/Notizen
Abstract
Parameterized programs are composed of an arbitrary number of concurrent, infinite-state threads. Automated safety and liveness proofs of such parameterized software are hard; state-of-the-art methods for their formal verification rely on intricate abstractions and complicated proof techniques that impede automation. In this paper, we introduce
thread-modular counter abstraction
(TMCA), a lean new abstraction technique to replace the existing heavy proof machinery. TMCA is a structured abstraction framework built from a novel combination of
counter abstraction
,
thread-modular reasoning
, and
predicate abstraction
. Its major strength lies in reducing the parameterized verification problem to the sequential setting, for which powerful proof procedures, efficient heuristics, and effective automated tools have been developed over the past decades. In this work, we first introduce the TMCA abstraction paradigm, then present a fully automated method for parameterized safety proofs, and finally discuss its application to automated termination and liveness proofs of parameterized software.