ALICE is one of the results of the Verisoft Project. The idea is coming from the P5 (Podelskis Pre- and Postcondition Pair Prover). Some short explanations of the project and P5 will follow.

Verisoft

The aim of the project of Verisoft is to fully verify a complete industrial system, beginning from hardware (processor) over an operating system (micro kernel and operating system) and a compiler to applications (email client). Such complete verification problems have not been finished so far. Most of the projects have only verified simple hardware and simple software so no complex system was tested before.

In this project a lot of verfication tools and environments have been build up. If everything will be finished in the future there will be one verification framework and every tool will be integrated into this environment. The interactive theorem prover Isabelle has been chosen as verification tool. Interactive tools have the advantage of generality at the price of low automatization. This means that you can express all relevant software problems and can show them if you are able to invest a lot of work for the interactive part.

Interactive theorem prover: Isabelle/HOL

Isabelle is a common and general theorem prover. The development of this tool started a long time ago and is developed even now. In contrast to other theorem provers the development did not stop so far. The long story is an advantage on one side: many people are using this theorem prover since its beginnings. The disadvantage is that some of the technics that were inserted at the beginning are no longer state of the art. Isabelle needs logics that represent the deductive system that can be used by Isabelle. One of the best developed logics is called HOL, higher order logic. The disadvantage for our project ist that you can not represent a imperative programming language. But to write lets say an email client you would prefer to have something like C.

Hoare logic

One of the most important steps in the project of Verisoft was the development of a logic that can represent an imperative program in the Isabelle environment. This logic is called Hoare because it does not only contain a representation of the C like code called C0, but a complete hoare calculus. Every program is written down as a hoare triple, namely a precondition that has to hold before the execution of the code, the code itself, and the postcondition that has to hold after the execution. The postcondition has to be verified, this proof obligation is called "functional property".

Other things that have to be shown are termination. This means that a function (or a complete program) has to terminate no matter about the input parameters. Otherwise a deadlock could apear. This is not wanted in the usual case.

A last type of errors that could occur are coming from the verification with Isabelle.Isabelle does not care about runtime errors like Null Pointer dereferencing or Integer overflows. To be able to check them a trick is used. Assertions are inserted to prevent the system from running in such error locations. Those assertions are inserted automatically by the logic.

To be able to use the higher order logic for the proofs a so called Verification Condition Generator (vcg) can be applied instead of other Isabelle tactics. This vcg generates logical formulas in HOL out of the program. The formulas represent the program and its proof obligations. It is sufficient to show them with classical methods known from HOL to proof the correctness of the system. This verification method needs a lot of time.

Automatic tools

Automatic tools in the verification process are mostly called software model checkers. This means that the automatic tool takes as input the source code of the program augmented with some proof obligations as assertions. The model checker tries to proof the correctness by different technics. Usualy there is some refinement step, which means that in the beginning the model used is very far away from the original program. If with this model verification is not possible, the tool tries to adjust the model. This circle is called refinement. Automatic tools usualy have three kinds of answers:

• YES, the proof obligation is fulfilled
• NO, the proof obligation is not fulfilled and there is a counter example
• I D'ONT KNOW, because there was no refinement step but no counter example could be found.

The "I d'ont know" case is explainable due to the fact that the problem is in NP. The automatic tools use simplified versions (the model) of the real world problem. This leads to a problem, that could occur: The tool could tell the verifier that the code is safe although it is not. If this problem occurs, the tool is called "unsound". The algorithms used in our tools are proven "sound".