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

 

The Faculty of Informatics is pleased to announce a seminar given by Grigory Fedyukovic.

 

 

Property Directed Equivalence via Abstract Simulation
 
Speaker: Grigory Fedyukovich
University of Washington, USA
Date: Wednesday, May 11, 2016
Place: USI Lugano Campus, room SI-013, Informatics building (Via G. Buffi 13)
Time: 13:30

 

Abstract:

In this talk, I present a novel approach for automated incremental verification that employs both reusable and relational specifications of software to incrementally verify pairs of programs with possibly nested loops. It analyzes two programs, P - the one already verified, and Q - the one needed to be verified, and proceeds by detecting an abstraction αP of P and a simulation ρ, such that αP simulates Q via ρ. The key idea behind our simulation synthesis is to drive construction of both αP and ρ by the safe inductive invariants of P, thus guaranteeing the property preservations by the results. Finally, our approach allows effective lifting of the safe inductive invariants of P to Q using only αP and ρ. Based on our evaluation, in many cases when the absolute equivalence between programs cannot be proven, our approach is able to establish the property directed equivalence, confirming that the program Q is safe.

 

Biography:

Grigory Fedyukovich is a postdoc at PLSE lab of University of Washington, USA, working with Prof. Rastislav Bodik. He completed the PhD at Formal Verification Lab of Universita della Svizzera Italiana (USI), Lugano, Switzerland (2015), under supervision of Prof. Natasha Sharygina. He graduated from Saint Petersburg State University, Russia (2008), and also did two internships at Institute of Cybernetics, Estonia (2009); and at National University of Singapore (2010).

The main focus of his research is Interpolation-based Incremental Model Checking, and Inductive Simulation Synthesis for establishing Program Equivalence.

 

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