This talk will discuss an application of Horn clauses solvers to software model checking. The first part reviews some problems in the state-of-art of the verification domain and describes one recent approach to automated unbounded verification. It will cover algorithms of encoding of programs into a system of Horn clauses and some approaches to solving them.
The second part will discuss the syntactic transformation of Horn clauses systems that can significantly relax the shape of the inductive invariant and makes a problem of its synthesis tractable for state-of-art Horn solvers in numerous cases. This transformation will be demonstrated on some programs with lists and non-linear arithmetics.
Presenter: Dmitry Mordvinov.
Date: April 10, 2017
Venue: room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28