ERCIM News No.36 - January 1999

Symbolic Techniques for Program Analysis

by Henk Nieland

---

As a consequence of our ever increasing dependence on the proper functioning of software systems, the need for proving their reliability has to be taken serious indeed. Until recently such proofs were only feasible for systems whose size is far below what is found in practice. Recently developed techniques, however, may offer a solution. The aim is now to apply these techniques effectively, so that real-life systems can be successfully analyzed. By combining mathematical rigour with manual computation CWI developed methods which can prove ‘beyond reasonable doubt’ the reliability of software systems of a realistic size.

In principle there are three approaches: proof by manual labour, fully automated proof techniques, and a mix between the two. CWI has shown that the last way enables the analysis of realistic systems.

Manual proof can be carried out in the context of Process Algebra (PA). The use of PA has advantages above other verification methods such as modal or temporal logic because of its high level of abstraction and its composition properties. A basic tool is the Cones & Foci Theorem, which effectively can be used to prove statements of the form: Specification = Implementation. On the basis of PA, CWI developed mCRL (micro Common Representation Language). The idea was to create a basis for sharpening symbolic techniques, rather than adding another language to the repertoire. With mCRL one can carry out proofs manually following strict logical rules. In practice, however, several such proofs remain ‘sloppy’, because the manual method is effective only for small systems, not exceeding one page of code.

Fully automated proof techniques are usually based on state automata. At CWI now systems with 108 states can be dealt with (in general the limit is 106), but realistic systems are still considerably larger. An even not really large system such as the software used for the safety of a small railway-yard, which was recently analyzed by CWI using propositional logic, consists of about 101000 states. Of course, it is of the utmost importance to find ways to reduce the number of states. Our research indicates that by transforming processes described in mCRL to a normal form (Linear Process Operation) using rewriting techniques (automated induction, tree automata), exponential reduction of the number of states can be reached.

Since neither purely manual, nor purely automated techniques can cope with realistic systems, a compromise must be sought. By using proof checkers, which guarantees the required precision, in combination with manual control, CWI has reached promising results. Experience with checkers like Coq, PVS, and Isabelle, used in this way, shows that this approach can be effective for middle-sized systems. One may compare this hybrid technique with the way packages such as MATLAB and MAPLE are used in mathematical formula manipulation. This approach to putting formal proof techniques to practical use may in due course very well lead to a revolution in mathematical argumentation, as was foreseen already some thirty years ago by the eminent Dutch mathematician N.G. de Bruijn when he created his Automath system.

Meanwhile several instances of faulty software have been revealed by applying formal proof checkers under manual control. Recent Dutch examples include the automated control system for the legs of car lifting installations in garages, and for the doors of the dam in the Nieuwe Waterweg which protects the Rotterdam area by closing the doors in case of flood. Sincs many more such instances can be expected to show up in the near future, we may see before long the birth of a new profession: that of software prover.

More information can be found at http://www.cwi.nl/~jfg/

Please contact:

Jan Friso Groote - CWI
Tel: +31 20 592 4232
E-mail: JanFriso.Groote@cwi.nl