POPL 2020 (series) / VMCAI 2020 (series) / VMCAI 2020 - 21st International Conference on Verification, Model Checking, and Abstract Interpretation /
Generalized Property-Directed Reachability for Hybrid Systems
Generalized property-directed reachability (GPDR) belongs to the family of the model-checking techniques called IC3/PDR. It has been successfully applied to software verification; for example, it is the core of Spacer, a state-of-the-art Horn-clause solver bundled with Z3. However, it has yet to be applied to hybrid systems, which involve a continuous evolution of values over time. As the first step towards GPDR- based model checking for hybrid systems, this paper formalizes HGPDR, an adaptation of GPDR to hybrid systems, and proves its soundness. We also implemented a semi-automated proof-of-concept verifier, which allows a user to provide hints to guide verification steps.
Mon 20 JanDisplayed time zone: Saskatchewan, Central America change
Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change
15:35 - 17:45 | |||
15:35 32mTalk | Cheap CTL Compassion in NuSMV VMCAI Daniel Hausmann Friedrich-Alexander-Universität Erlangen-Nürnberg, Tadeusz Litak FAU Erlangen-Nuremberg, INF 8, Christoph Rauch FAU Erlangen-Nürnberg, Lehrstuhl 8, Matthias Zinner FAU Erlangen-Nürnberg | ||
16:07 32mTalk | A Cooperative Parallelization Approach for Property-Directed k-Induction VMCAI Martin Blicha Università della Svizzera italiana, Antti Hyvärinen Università della Svizzera Italiana, Matteo Marescotti Università della Svizzera Italiana, Natasha Sharygina USI Lugano, Switzerland | ||
16:40 32mCoffee break | Mini Break VMCAI | ||
17:12 32mTalk | Generalized Property-Directed Reachability for Hybrid Systems VMCAI Link to publication Pre-print |