Floating Point Model Checking

We at Prover are very happy to announce the release of version 4.0 of our model checker Prover SL CE (PSL). The most interesting new feature is support for IEEE 754 floating point calculations, so I will dedicate this technical blog post to floats with a concrete example of a floating point system which we analyze using PSL.

Floating point example – an exotic investment

To illustrate the usefulness of floats inside our model checker, we will define a non-trivial investment game, formalize it in an extension of HLL (the input language of PSL), and check some properties of the investment using PSL. The rules of the investment are as follows:

1. The initial investment is 100.0 of our favorite currency (let’s call it “satcoins”).
2. A year of normal return, our investment grows with 5 %.
3. A good year, which happens at least once every 5 years, the investment grows with 20 % plus an extra bonus of 0 to 100 satcoins.
4. A bad year, which also happens at least once every 5 years, the investment is halved.
5. An excellent year, which happens at least once every 7 years, the invested amount is squared (multiplied by itself).
6. Finally, a disastrous year, which happens at least once every 8 years, cancels the result of an excellent year: the new amount is the quotient of the current amount and that of the previous year.
7. The first year is a normal year.
8. An excellent or disastrous year is always followed by a bad year.
9. The calculations shall be performed according to the international floating point standard IEEE 754 using 32-bit binary floats (known as the type “float” in the C programming language).

This informal specification of the investment rules can be straightforwardly translated into extended HLL. We will omit some of the details. However, the part relating to the actual floating point calculations could be formalized into the following code:

@ include FP_8_23
Namespaces:
FP_8_23 {
 Types:
  enum {normal, good, bad, excellent, disastrous} Year;
 Declarations:
  Year year;
  int [0, 100] bonus;
  float amount;
 Definitions:
  rne := Rounding::rne;     // Round to nearest tie to even
  I(amount) := 100.0;
  X(amount) := (year
               |normal     => mul(rne, amount, 1.05)
               |good       => add(rne, mul(rne, amount, 1.2),
                                       of_int(rne, bonus))
	       |bad        => div(rne, amount, 2.0)
	       |excellent  => mul(rne, amount, amount)
	       |disastrous => div(rne, amount, pre(amount)));
}

Checking properties of our investment

The kind of properties of floating point calculations that we are interested in checking using our model checker, is typically properties such as “the calculation does not overflow our 32-bit representation (no infinities)” and “divisions by zero does not happen (no NaN values appear)”. Indeed, PSL is able to prove the absence of overflow and NaN for the first 80 years of our investment over night. Note that properties such as “the expected average return on investment” is outside of the realm of model checking, and so will not be considered here. Instead, we will ask PSL if our investment can generate (if we’re lucky) at least a billion satcoins. We do this, as usual, by trying to prove that the amount on our account is always less than a billion. If the tool disproves (or falsifies) this property, then it will provide a counterexample to the proof as a solution:

Proof Obligations:
 lt(amount, 1.0e9);

In a matter of minutes, in single thread on an average laptop, PSL tells us that after at least 13 years, there exists a scenario in which we become satcoin billionaires. (In this time, PSL has also proved that there are no scenarios shorter than 13 years.) Below is one out of many scenarios found by PSL. The table should be read by combining the “year”, “bonus” and “amount” on the same line to determine the “amount” on the next line. As usual when dealing with automatic provers, the scenario may surprise at first, but is nevertheless valid and easily verified.

Summary

We have shown how a non-trivial floating point calculation, in the guise of an investment game, can be successfully checked by PSL 4.0. It should be noted, however, that automatic verification of floating point arithmetic is notoriously hard, and there are numerous pitfalls, so it is important to have realistic expectations. PSL uses underlying techniques known as bitblasting and SAT-solving, which are extremely precise (down to the last bit), but of course come with an attached cost. For example, if we double the precision from 32-bit to 64-bit floats in our investment game, runtimes approximately quadruple. Fortunately, PSL provides very efficient support for parallel computing, which means that such effects on runtime can be compensated by the use of more processor cores.

We conclude by observing that for complex safety-critical reactive systems with a little bit of floating point arithmetic, automatic reasoning tools such as PSL can be very useful, especially for finding unexpected scenarios such as the generation of NaN, infinities and other values out of the expected range.