Code Validation

Object code is an important part of safety-critical systems. Many risks associated with computing systems are due to the possible presence of errors. Some of these potential errors may be due to improper coding of programs in the high-level programming languages, while others may arise through the interaction between the abstract program and the environment (operating system, compiler, etc.) in which the program runs. By verifying object code, one may increase assurance about the correct running of the program. However, object code has traditionally been considered difficult to reason about, due to the large sizes of the resulting descriptions and lack of automated tools, resulting in large amount of effort in verifying even small programs. Assurance of quality of object code is an important aspect of risk management, in both industry and government, around the world. The aim of this research is the development of a paradigm for the practical verification of object code.

The research performed by our group has resulted in the development of tools for bringing together several theoretical strands and partially successful methodologies for verification. We have developed translators between temporal-logic based and process-algebra based reasoning, a tool for the formalisation of code for the MC68K architecture, a tool for rigorous reasoning with numbers in the Isabelle theorem prover.

Staff involved: Sara Kalvala