Abstract:

We have developed and successfully applied a technique to build a high integrity compiler from Pasp, a non-trivial Pascal-like language, to Asp, the target language for a high integrity processor designed for the UK's Atomic Weapons Establishment at Aldermaston.

We overview the technique itself, including a description of how it can be extended to separate compilation. We also describe some of our experiences whilst implementing this compiler, how successful the whole process has been, and the lessons we have learned.

We have cost-effectively developed a compiler to high integrity by using mathematical specification and proof techniques.

@inproceedings(SS-HASE98,
  author = "Susan Stepney",
  title = "Incremental Development of a High Integrity Compiler:
           experience from an industrial development",
  crossref = "HASE98"
)

@proceedings(HASE98,
  title = "Third IEEE High-Assurance Systems Engineering Symposium (HASE'98),
           Washington DC, USA",
  booktitle = "Third IEEE High-Assurance Systems Engineering Symposium (HASE'98),
              Washington DC, USA",
  year = 1998
)