The Core of the Core

by Johannes Kanig in Formal Verification, Open Source – June 11, 2013

Yesterday, I attended the PhD thesis Defence of Mohamed Iguernelala at the lab of the research team Toccata at INRIA, France. Mohamed has done a lot of work on the SMT prover Alt-Ergo which is used in SPARK 2014.

An SMT prover is a program that can prove mathematical formulas. The special thing about an SMT prover, compared to other prover families, is that it can handle very well not only truth values (true and false) but also with data such as integers, arrays, records and so on.

Mohamed has worked at the very core of Alt-Ergo, and his PhD thesis brings, among a number of smaller enhancements, two major improvements to the prover and the theory of SMT provers in general.

The first one is about reasoning about linear arithmetic, that is about inequations of the form

  ax + by <= c

The difficulty is to decide if a set of such equation actually admits a solution for variables such as x and y, and in particular if there is a solution where x and y are integers and not rational numbers.

There are two main methods to solve such equations: the Fourier-Motzkin algorithm and the Simplex method. Fourier-Motzkin is the one that Alt-ergo uses because is easy to implement, and it has the advantage to be easy to extend to the case for integers. Also, it is easy to extract information about intervals from the answer of the algorithm. But Fourier-Motzkin is both slow and costly in memory consumption. A much more efficient method is the Simplex algorithm, but it is harder to implement and loses much of its efficiency if extended to the integer case. Extracting interval information is not possible.

Mohamed has found a way to combine the advantages of both ideas: he uses the faster Simplex method to *simulate* a run of the Fourier-Motzkin algorithm. Extracting interval information from this run is still possible, and he showed that with this idea, a modified version of Alt-Ergo is much faster than existing tools on common problems that involve inequations with linear arithmetic.

His second contribution is about associative and commutative symbols such as multiplication, or set union, or many other symbols. The simple way of supporting such symbols is through axioms which express the associativity and commutativity properties of these symbols. However, this method is very inefficient even on small examples. Mohamed has presented and implemented in Alt-Ergo a way to efficiently handle such symbols through a technique which combines the data reasoning of SMT provers with a common technique for associative and commutative symbols, namely ground AC completion.

What has all of this to do with SPARK 2014? Today, Alt-Ergo is in fact at the core of the SPARK 2014 toolset, so any improvement of Alt-Ergo directly benefits SPARK users. Actually, at the closing meeting of the Hi-Lite project, Mohamed has shown that Alt-ergo has improved a lot over the 3-year period of the project. Mohamed's work is in part responsible for this improvement, through the addition of more supported data types in Alt-ergo, such as arrays and enumerated types and the work on associative and commutative symbols. The work about integer arithmetic is also expected to be integrated in the main branch, so we can expect more improvements in the future.

comments powered by Disqus