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


The Faculty of Informatics is pleased to announce a seminar given by Pierre Roux



Solving Non-Linear Arithmetic: a Numerical Alternative
Speaker: Pierre Roux
ONERA, France
Date: Friday, October 28, 2016
Place: USI Lugano Campus, room SI-015, Informatics building (Via G. Buffi 13)
Time: 10.30



State-of-the-art (semi-)decision procedures for non-linear arithmetic address polynomial inequalities by mean of symbolic methods, such as quantifier elimination. Although (some of) these methods offer nice completeness properties, their high complexity remains a limit, despite the impressive efficiency of modern implementations. This appears, for instance, to be an obstacle to the use of SMT solvers for the verification of functional properties of control-command programs.
We offer an alternative method that uses off-the-shelf numerical optimization solvers. These solvers only deliver approximate solutions and cannot be trusted due to the algorithms they implement. Nonetheless, while this prevents the completeness of our approach, its soundness is guaranteed by an efficient a-posteriori validation method. Our early prototype implemented in the Alt-Ergo SMT solver already gives some impressive results, particularly on control-command programs.



Pierre Roux completed in 2013 a PhD in static analysis on automatic inference of ellipsoidal invariants for control-command programs, using numerical optimization solvers. He then discovered the proof assistant Coq during a postdoc at LRI/INRIA Saclay with Sylvie Boldo and Guillaume Melquiond, proving with it some algorithm based on floating-point arithmetic. After a second postdoc at CU Boulder with Sriram Sankaranarayanan on the inference of polynomial invariants, he is now a research engineer at ONERA, the french public agency for aerospace research, in Toulouse.


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