Learning Invariants for Verification of Programs and Control Systems

Abstract

Deductive verification techniques in the style of Floyd and Hoare have the potential to give us concise, compositional, and scalable proofs of the correctness of various kinds of software systems like programs and control systems. However, the major hurdle in adopting these techniques is that the verification engineer often needs to come up with adequate program invariants (like loop invariants), which may require a lot of expertise and manual effort. This thesis tries to address this problem by attempting to automate the process of finding adequate invariants, using machine learning and other techniques.

In the first part of this thesis, we introduce a data-driven learning-based technique to automate the computation of adequate invariants for the deductive verification of various classes of programs, including recursive sequential programs, and concurrent programs. We consider standard pre-post specifications for these programs. Deductive verification of programs can be viewed as finding a solution to a system of Constrained Horn Clauses (CHCs) induced by the program and its specification. Earlier works on data-driven learning of invariants like ICE learning (Garg et al, 2014) can only handle linear CHCs. However, many deductive verification techniques like Requires-Ensures (for recursive sequential programs) and Rely-Guarantee and Owicki-Gries (for concurrent programs) induce non-linear CHCs. We propose a technique called Horn-ICE, which extends the ICE learning technique to solve non-linear CHCs, thereby allowing us to automate the deductive verification of a variety of new classes of programs.

Non-linear CHCs give rise to Horn implications counterexamples (Horn clauses) in general, so our learning setup considers a semi-labelled dataset along with its metadata in the form of Horn clauses. We have implemented a decision tree based classifier for this semi-labelled dataset. This classifier learns candidate invariants for a deductive verification task. We demonstrate the performance of this automated program verification technique using standard benchmarks like SV-COMP. On the sequential benchmark suite, our tool is on par with the state of the art tool Z3/PDR. On the recursive benchmark suite, we outperform the state of the art tool Ultimate Automizer (Heizmann et al, 2013) . On the concurrent benchmark suite, we are able to verify all of the programs within a few seconds.

In the second part of this thesis, we consider sampled-data control systems that control a continuous plant using a discrete controller, and the band convergence property for these systems. Our first contribution in this part of the thesis is a deductive verification technique for sampled-data control systems. This technique symbolically executes the system from the initial state onwards until an adequate invariant is reached. For this verification technique, we developed a concolic execution based white-box approach for learning adequate invariants. We demonstrate the performance of our automated sampled-data control system verification technique using standard Simulink models. Our toolchain is able to verify band convergence properties for most of these models within a few seconds.