Write a Blog >>
Mon 20 Jan 2020 17:12 - 17:45 at St Jerome - Papers 5 Chair(s): Nikolaj Bjørner

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 Jan

Displayed time zone: Saskatchewan, Central America change

15:35 - 17:45
Papers 5VMCAI at St Jerome
Chair(s): Nikolaj Bjørner Microsoft Research
15:35
32m
Talk
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
32m
Talk
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
32m
Coffee break
Mini Break
VMCAI

17:12
32m
Talk
Generalized Property-Directed Reachability for Hybrid Systems
VMCAI
Kohei Suenaga Graduate School of Informatics, Kyoto University, Takuya Ishizawa Kyoto University
Link to publication Pre-print