Solving Non-Linear Arithmetic: a Numerical Alternative

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.
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.

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.