Generalized Property-Directed Reachability for Hybrid Systems

TL;DR

This paper extends the GPDR model-checking technique to hybrid systems, formalizes HGPDR, proves its soundness, and provides a semi-automated verifier to aid hybrid system verification.

Contribution

It introduces HGPDR, the first adaptation of GPDR for hybrid systems, including formalization, soundness proof, and a semi-automated verification tool.

Findings

HGPDR is sound for hybrid systems.

A semi-automated verifier was implemented.

The approach facilitates hybrid system verification.

Abstract

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.