Description

BetterBe is a company, based in Enschede, that provides webservices to automotive lease companies, in particular, calculates the price of a particular lease car.

Calculating this price is more complex than one may think, merely because of the large number of intricate dependencies between the various options. For instance: if you opt for a sports package, you cannot choose certain radios (reason: the leather steering wheel coat does not have the right holes for the radio buttons). There are hundreds of such dependency rules. Therefore, figuring out if a certain set of option is feasible, and determine its price, is non-trivial.

Two aspects of the price calculation are very important: speed and correctness.

Speed of this price calculation is of utmost importance: every click in a car leasing website triggers a lease calculation, which must be fast, for users to have a pleasant user experience. But even more important than speed is correctness. Users may not lease cars when the calculated prices are too high, and leasing companies may make huge losses when the calculated prices are too low.

To achieve speed of calculation, BetterBe builds its software using a number of efficient basic data structures, of which a red-black tree and a multi-hash-table are the most important. Correctness of the implementation of these basic data structures is is thus very important, not only to obtain correct price calculations, but also to obtain them as fast as possible: performance may seriously suffer when red-black trees loose their balance.

Formal verification using static analysis techniques is seen as possible solution that may give BetterBe rigorous proof of correctness, or clear indication of errors.
In practice, this means (1) to formulate invariants to which the data structures have to comply, and (2) to show that the data structures do not invalidate these invariants. In an earlier MSc project, a standard red-black tree data structure has been proven (functionally) correct, as a first step in this project. The current project is about taking the next step, and adapting the standard data structure towards the specific data structure used at BetterBe.