Solving Non-Linear Arithmetic: a Numerical Alternative
Staff - Faculty of Informatics
Start date: 28 October 2016
End date: 29 October 2016
|
|||||||||||
|
|||||||||||
Abstract: |
|||||||||||
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. |
|||||||||||
|
|||||||||||
Biography: |
|||||||||||
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. |
|||||||||||
|
|||||||||||
|