Seminars

View all Seminars  |  Download ICal for this event

Data-driven verification of procedural programs with integer arrays

Series: CSA Distinguished Lecture

Speaker: Ahmed Bouajjani

Date/Time: Jan 23 11:30:00

Location: CSA Auditorium, (Room No. 104, Ground Floor)

Abstract:
We address the problem of verifying automatically procedural programs manipulating parametric-size arrays of integers, encoded as a constrained Horn clauses solving problem. We propose an algorithmic method for synthesizing loop invariants and procedure pre/post-conditions represented as universally quantified first-order formulas constraining the array elements and program variables. We adopt a data-driven approach that extends the decision tree Horn-ICE framework to handle arrays. We provide a new learning technique based on reducing a complex classification problem of vectors of integer arrays to a simpler classification problem of vectors of integers. The obtained classifier is generalized to get universally quantified invariants and procedure pre/post-conditions. We have implemented our method and shown its efficiency and competitiveness w.r.t. state-of-the-art tools on a significant benchmark.

This is a joint work with Wael-Amine Boutglay and Peter Hebermehl.

Speaker Bio:
Ahmed Bouajjani is a Professor at Univ. Paris Diderot and a Senior Member of the Institut Universitaire de France. He is well known for his work on verification of infinite-state systems, concurrency, automata and logic.

Host Faculty: Deepak D'Souza