Department of Computer Sciences 1999 ACL2 Workshop March 29 - March 31, 1999

Proving the correctness of an Embedded Verifier for a Safety-Critical translator

We describe the use of ACL2 within the frame of an industrial project aimed at verifying the correct behaviour of a translator called Gem2Rtm. Gem2Rtm is used to generate safety-critical trainborne control software. To achieve the desired result we designed an independent piece of software, called the Embedded Verifier. The Embedded Verifier checks each Gem2Rtm translation on-line, by verifying that Gem2Rtm's inputs and outputs obey a number of ``syntactic'' correspondence conditions. The syntactic nature of the checks allows the verification to be automatic and efficient.

We are using ACL2 to prove the correctness of the Embedded Verifier, i.e. to guarantee that the syntactic cheks it performs are sufficient to guarantee that no incorrect translations are accepted. We report on the current status of the mechanization, focusing on the main theorem proved so far, and we describe a workplan to complete the mechanization.

Slides (use "Swap Landscape" when in ghostview)

• One slide per page

Piergiorgio Bertoli