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.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{ZimmermannKSW24,
author = {Wolf Zimmermann and
Thomas K{\"{u}}hn and
Edward Sabinus and
Mandy Wei{\ss}bach},
editor = {Silvia Bonfanti and
Angelo Gargantini and
Michael Leuschel and
Elvinia Riccobene and
Patrizia Scandurra},
title = {Small Step Incremental Verification of Compilers},
booktitle = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14759},
pages = {262--269},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-63790-2\_21},
doi = {10.1007/978-3-031-63790-2\_21},
timestamp = {Fri, 13 Sep 2024 16:19:49 +0200},
biburl = {https://dblp.org/rec/conf/zum/ZimmermannKSW24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}