Abstract State Machines




ASM Studies

Compiler Back-ends

Citation: Wolf Zimmerman, and Thilo Gaul, "On the Construction of Correct Compiler Back-Ends: An ASM Approach", Journal of Universal Computer Science, vol. 3, no. 5 (1997), 504--567.
Summary: The authors use ASMs to construct provably correct compiler back-ends based on realistic intermediate languages (and check the correctness of their proofs using PVS).
Subjects: Compiler Correctness, Mechanical Verification, Verification
Download: PostScript, PDF, Compressed PostScript
Notes: Courtesy of Springer-Verlag.