Small Step Incremental Verification of Compilers

Previously, we introduced the idea of agile compiler development, i.e., starting from an initial compiler for the most simple program of a language and extending it in small versions, each introducing a new language concept. Following this idea, in this paper, we propose an approach for incrementally verifying the dynamic semantics specified with abstract state machines (ASMs), such that definitions of previous versions must not be altered in subsequent versions. As a result, the compiler can be verified incrementally without revising the proofs of previous versions. As our first step, in this paper, we formalize and verify the memory mapping of the initial versions with ASMs and discuss their extensibility for the next increments. We plan to demonstrate this approach through the agile implementation and verification of a Sather-K compiler generating MIPS assembly language.