VerComp is closely related to the joint project Verifix, which tackles the correct construction of compilers and compiler generators.
In Vercomp we focus on Correct Compiler Implementation, e.g. the question, why the actual compiler program in binary machine code really correctly translate source programs into target programs.
Our aim is to develop a technique to win fully correct compilers for realistic programming languages and for real target hardware, that is compilers for which all of the aspects:
We defined a small applicative programming language, ComLisp, which is a subset of ANSI-CommonLisp. A modular compiler translates ComLisp programs via the intermediate languages SIL, Cint, and TASM down to binary machine code TC of our target machine (which for historical reasons currently is an inmos transputer, but need not be). This compiler is written (correctly constructed) in ComLisp, i.e. its own source language.
To verify the implementation of the ComLisp to TC compiler, we bootstrap it twice, starting with a contemporary CommonLisp implementation. In effect the binary machine code compiler program will be generated following our compiling specification. Unfortunately any mistakes done in the contemporary CommonLisp implementation could lead to a malfunctioning binary compiler program, so we have to assure the binary program is generated in every detail according to our specification. We do this by doublechecking the results of the single compiler bootstrap run on a purely syntactical level.
We prepare all transitions that need to be inspected in certification documents where source program fragments and their corresponding target program fragments are printed side by side to ease the inspection and thus the whole compiler implementation proof.
Interested in more information and discussion? Please get in contact with me.