Skip to main content

Seminar:  Algorithmic Logic-Based Verification

Date:April 27, 2015 
Talk Title:Algorithmic Logic-Based Verification
Speaker:Temesghen Kahsai, Research Scientist at NASA Ames Research Center
Time & Location:12:00pm - 1:00pm
Panther Hollow Room, CIC Building, Pittsburgh

Abstract

Developing new tools for automated software verification is a tedious and very difficult task. First, due to the undecidability of the verification problem, tools must be highly tuned and engineered to provide reasonable efficiency and precision trade-offs. Second, different programming languages comes with very diverse assortments of syntactic and semantic features. Third, the diverse encoding of the verification problem makes the integration with other powerful solvers and verifiers difficult.

To mitigate these challenges, in this talk, I will present SeaHorn, an LLVM-based software verification framework that allows the decoupling of programming language syntax and semantics from the underlying verification technique. Such framework uses Horn Clauses as the intermediate formal language for the verification task. Horn Clauses are a uniform way to encode verification conditions. SeaHorn solves much of the programming language complexities by borrowing techniques and implementation from an optimizing compiler. SeaHorn is versatile and highly customizable framework which allows researchers to easily build or experiment their particular verification techniques of interest. I will also illustrate experimental evaluation that demonstrate the competitiveness of SeaHorn in verifying safety properties.

Speaker Bio

Temesghen Kahsai is a research scientist at NASA Ames employed by CMU, where he has been a member of the Robust Software Engineering group since 2013. 

His research interests are in the automated software analysis for complex safety and mission critical software. From 2012 to 2013, he was a software engineer at Skype (Microsoft), where he worked on the mobile core division. From 2010 to 2012, he was a postdoctoral research scholar at the University of Iowa, where he worked on scaling SMT-based model checking. He is currently leading three research projects funded by NASA and NSF on contract-based verification of outsourced flight critical systems, compositional analysis of heterogeneous software protocol stack and credible auto-coding of embedded systems. 

Education:

PhD, 2011. Computer Science, Swansea University, Wales, UK.
MS, 2006. Computer Science, University of Udine, Italy
BS, 2003. Computer Science, University of Udine, Italy

Web:

www.lememta.info