If you do not see this message displayed properly, please click here


The Faculty of Informatics is pleased to announce a seminar given by Arie Gurfinkel.



Algorithmic Logic-Based Verification with SeaHorn
Speaker: Arie Gurfinkel
University of Waterloo, Canada
Date: Thursday, October 6, 2016
Place: USI Lugano Campus, room SI-004, Informatics building (Via G. Buffi 13)
Time: 13:30



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 eveloping new software verification techniques.




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.


Host: Prof. Natasha Sharygina


Faculty of Informatics

Faculty of Informatics
Università della Svizzera italiana
Via Giuseppe Buffi 13
CH-6904 Lugano
Tel.: +41 (0)58 666 46 90
Fax: +41 (0)58 666 45 36
Email: decanato.inf@usi.ch
Web: www.inf.usi.ch
Twitter: @USI_INF


Segui USI@EXPO2015 su Twitter Segui USI@EXPO2015 su Facebook Segui USI@EXPO2015 su Linkedin Segui USI@EXPO2015 su YouTube