Abstract State Machines




ASM Studies

Compiler Back-end Rewrite Systems

Citation: Axel Dold, Thilo Gaul, Vincent Vialard, and Wolf Zimmerman, "ASM-Based Mechanized Verification of Compiler Back-Ends". In Proceedings of the 28th Annual Conference of the German Society of Computer Science, Technical Report, Magdeburg University, 1998.
Summary: An approach for mechanically proving the correctness of back-end rewrite system (BURS) specifications is described. This approach can be used in conjunction with BURS-based back-end compiler generators. PVS is used to perform the mechanical verification.
Subjects: Compiler Correctness, Mechanical Verification
Download: PostScript, PDF, Compressed PostScript