KIT | KIT-Bibliothek | Impressum | Datenschutz

Pegasus: sound continuous invariant generation

Sogokon, Andrew ; Mitsch, Stefan; Tan, Yong Kiam; Cordwell, Katherine; Platzer, André ORCID iD icon

Abstract:

Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.


Verlagsausgabe §
DOI: 10.5445/IR/1000174214
Veröffentlicht am 16.09.2024
Originalveröffentlichung
DOI: 10.1007/s10703-020-00355-z
Scopus
Zitationen: 9
Web of Science
Zitationen: 6
Dimensions
Zitationen: 11
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Informationssicherheit und Verlässlichkeit (KASTEL)
Publikationstyp Zeitschriftenaufsatz
Publikationsmonat/-jahr 10.2021
Sprache Englisch
Identifikator ISSN: 0925-9856, 1572-8102
KITopen-ID: 1000174214
Erschienen in Formal Methods in System Design
Verlag Springer
Band 58
Heft 1-2
Seiten 5–41
Vorab online veröffentlicht am 20.01.2021
Schlagwörter Invariant generation, Continuous invariants, Ordinary differential equations, Theorem proving
Nachgewiesen in Scopus
Web of Science
Dimensions
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page