• People
• Events
• Research

Correctness Proofs of Compilers and Debuggers: an Overview of an Approach Based on Structural Operational Semantics

Abstract: This paper is an overview of the main results presented in the author's Ph.D. thesis [dS92]. In this paper we study the use of semantics-based formal methods in the specification and proof of correctness of compilers and debuggers. We use a Structural Operational Semantics as the basis for the specification of compilers and propose a notion of correctness based on an observational equivalence relation [ST87]. We define program evaluation and a notion of evaluation step based on a Structural Operational Semantics and use these definitions as the basis for the specification of debuggers. Debugger correctness is then defined by an equivalence relation between a specification and an implementation of the debugger based on the bisimulation concept [Par81].

LFCS report ECS-LFCS-92-233