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 Fedyukovich



Witnessing existential quantifiers with AE-VAL
Speaker: Grigory Fedyukovich
University of Washington, USA
Date: Thursday, October 20, 2016
Place: USI Lugano Campus, room SI-015, Informatics building (Via G. Buffi 13)
Time: 14:30



Various tasks in formal verification and synthesis rely on efficient techniques to remove existential quantifiers from formulas in First Order Logic. Additionally, modern quantifier elimination approaches are able to produce Skolem functions witnessing existential quantifiers. I present AE-VAL, a decision procedure for Linear Rational Arithmetic that enumerates models for quantified formulas and automatically constructs Skolem functions. In the talk, I demonstrate the use of AE-VAL for the tasks of "Realizability Checking and Synthesis of Contracts" and "Automatic Discovery of Simulation Relations".



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, 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 Software Model Checking, and Synthesis.


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