Arie Gurfinkel
Algorithmic Logic-Based Verification with SeaHorn
November 16, 2016 at 3:30pm CSE 305
Abstract
Program verification, e.g., synthesis of safe inductive invariants, is a long standing challenge in Computer Science. While the problem is undecidable in general, there are many automated techniques that perform well in practice. In this talk, I will present SeaHorn – a software verification framework for C programs. A key distinguishing feature of SeaHorn is a modular design that decouples the concerns of the syntax of the programming language, from its operational and verification semantics. Ideally, operational and verification semantics must coincide. However, this is extremely difficult to achieve in practice. SeaHorn extends software verification in several ways: (a) it contributes an efficient yet precise inter-procedural SMT-based verification algorithm, (b) it provides flexible verification semantics with support for different levels of precision and abstraction, (c) it successfully combines software model checking and abstract interpretation, and (d) it uses the logic of Constrained Horn Clauses as its intermediate verification language. SeaHorn provides the users of verification with a powerful automated verification tool. At the same time, it is extensible and customizable framework for experimenting with and developing new software verification techniques.
Bio
Arie Gurfinkel received a Ph.D. in Computer Science from the Computer Science Department of University of Toronto in 2007. He is an Associate Professor at the Department of Electrical and Computer Engineering at the University of Waterloo. Until 2016, he was a Principle Researcher at the Carnegie Mellon Software Engineering Institute. His research interests lie in the intersection of formal methods and software engineering, with an emphasis on automated reasoning about software systems. He has co-lead development of a number of automated verification tools including the first multi-valued model-checker XChek, award winning software verification frameworks UFO and SeaHorn, and a hardware model-checker Avy.