Seminars

View all Seminars  |  Download ICal for this event

Learning Invariants for Verification of Programs and Control Systems

Series: Ph.D. (Engg.) Colloquium- ONLINE

Speaker: Mr. P. EzudheenPh.D (Engg.) studentDept. of CSA

Date/Time: Mar 11 10:00:00

Location: Online on Google Meet: https://meet.google.com/gvp-wzwd-tcp

Faculty Advisor: Prof. Deepak DSouza

Abstract:
Learning Invariants for Verification of Programs and Control Systems
<br>
Abstract:
<br>
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. We try to address this
problem by attempting to automate the process of finding adequate
invariants, using machine learning and other techniques.
<br>
In the first part of the presentation, 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.
<br>
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
some popular programs within a few seconds.
<br>
In the second part of the presentation, 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 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.
<br>
Details for joining online on Google Meet:
<br>
Link: <a href="Link