The area of software verification has grown its importance in software engineering. This is a
bibliography of verification of a specialized class of softwares called compiler. The citations …

Compilers that have been formally verified in theorem provers are often not directly usable
because the formalization language is not a general-purpose programming language or the …

This article presents a type certifying compiler for a subset of Java and proves the type
correctness of the bytecode it generates in the proof assistant Isabelle. The proof is …

This paper reports on a large verification effort in constructing an initial fully trusted bootstrap
compiler executable for a realistic system programming language and real target processor …

The theory of relative program correctness and its preservation allows for elaborate and
practically adequate definitions of correct implementation notions as they are established by …

Compilers are large and complex pieces of software, which can be challenging to work with.
Modularity has significant benefits in such cases: building a complex system from a series of …

The article starts out from the observation that software engineering splits in two large
activity areas: Software specification with its verification and software implementation with its …

Abstract Trojan horses of Thompson-Goerigk-type are intended software errors very hidden
in machine level compiler implementations although the latter have successfully passed …

We present lessons learned from using mechanical theorem proving for proof support in
software verification, with trusted execution of programs in mind. We will use two realistic …

Bibtex Entries for the ACL2 Workshops Page 1 Bibtex Entries for the ACL2 Workshops
Jared Davis February 24, 2005 This file provides a list of bibtex entries which can be used …