Peter H. Schmitt · KITopen · 1994
In this note we analyse the proof of compiler correctness of the WAM given in the paper The WAM - Definition and Compiler Correctness by Egon Boerger and Dean Rosenzweig. TR-14/92, Dipartimento di Informatica, Universita di Pisa, 1992. with regard to the question how it could be assisted by an automated theorem prover. We will give further details of the proof methodology and present the proof obligations in a form that is amenable to automated deduction systems.
Cited by 7Open access
James R. Larus · 2011
No abstract available.
Cited by 0
H. Bekić · Lecture notes in computer science · 2006
Cited by 0
Kuen-bang Hou (favonia, Robert Harper · 2013
Type refinements, introduced by Freeman and Pfenning and explored by Davies and Dunfield, unify the ontological and epistemic views of typing. Types tell us what programming language constructs exist, whereas refinements express properties of the values of a type. Here we show that refinements are very useful in compiler correctness proofs, wherein it often arises that two expressions that are inequivalent in general are equivalent in the particular context in which they occur. Refinements serve to restrict the contexts sufficiently so that the desired equivalence holds. For example, an expression might be replaced by a more efficient one, even though it is not generally equivalent to the original, but is interchangeable in any context satisfying a specified refinement of the type of those expressions. We study here in detail a particular problem of compiler correctness, namely the correctness of compiling polymorphism (generics) to dynamic types by treating values of variable type as values of a universal dynamic type. Although this technique is widely used (for example, to compile Java generics), no proof of its correctness has been given to date. Surprisingly, standard arguments based on logical relations do not suffice, precisely because it is necessary to record deeper invariants about the compiled code than is expressible in their types alone. We show that refinements provide an elegant solution to this problem by capturing the required invariants so that a critical invertibility property that is false is general can be proved to hold in the contexts that arise in the translated code. This proof not only establishes the correctness of this compilation method, but also exemplifies the importance of refinements for compiler correctness proofs more generally.
Cited by 0
Of The College · 2007
The goal of my thesis is to extend current methods for compiler derivation and verification to languages which exhibit true concurrency. The work has proceeded through the following steps. A process calculus, called CLAM, was defined, based on the -calculus and modelling true concurrency. CLAM was used to define the semantics of a simple concurrent functional language, called Urlang, which was inspired by the programming language Erlang, which is in industrial use. A bytecode compiler for Urlang was then derived and proven correct, and a multiprocessor bytecode interpreter was implemented in Concert/C and proven correct. Finally it is argued that those features of Erlang which are not present in Urlang are easily added into our framework, either via source-to-source transformations into core Urlang or by means of straightforward additions to the operational semantics of CLAM. vii viii Acknowledgments This thesis would not have been possible without my advisor, Mitchell Wand. I tha...
Cited by 0
David William John Stringer-Calvert · 1998
A large investment is made in the development, testing, validation and verification of source code for critical applications. But there remains a semantic gap between the source code produced and the object code which is executed. Standards for the development of critical systems recognize this, and mandate either the use of a trusted compiler (one that has been proven to produce correct object code) or the demonstration that the object code is a correct refinement of the source code (a lengthy and complex process). This thesis examines: 1. the extent to which tool support is an essential ingredient in proofs of compiler correctness; 2. the extent to which these proofs may be automated; 3. the relationship between the complexity of the source language and the proof effort required; 4. the scalability of a mechanical method of compiler verification. To do this, we present the development of the proof of correctness of a compiler for a small imperative language Tosca, targeted at an imag...
Cited by 0
Andrew W. Appel, Robert Dockins · 2012
Compilers are an essential part of the software development process. Programmers all over the world rely on compilers every day to correctly translate their intentions, expressed as high-level source code, into executable low-level machine code. But what does it mean for a compiler to be correct?
This question is surprisingly difficult to answer. Despite the fact that various groups have made concerted efforts to prove the correctness of compilers since at least the early 1980's, no clear consensus has arisen about what it means for a compiler to be correct. As a result, it seems that no two compiler verification efforts have stated their correctness theorems in the same way.
In this dissertation, I will advance a new approach to compiler correctness based on refinements of the operational semantics of programs. The cornerstones of this approach are behavioral refinement, which allows programs to improve by going wrong less often, and choice refinement, which allows compilers to reduce the amount of internal nondeterminism present in a program. I take particular care to explain why these notions of refinement are the correct formal interpretations of the informal ideas above.
In addition, I will show how these notions of refinement can be realistically applied to compiler verification efforts. First, I will present a toy language, WHILE-C, and show how choice and behavioral refinement can be used to verify the correctness of several interesting program transformations. The WHILE-C language and the transformations themselves are simple enough to be presented here in full detail. I will also show how the ideas of behavioral and choice refinement may be applied to the CompCert formally verified compiler, a realistic compiler for a significant subset of C.
Cited by 7
B.v. Karger · Elsevier eBooks · 1990
Cited by 0
Shahrzade Mazaher · 1982
Cited by 2
Paul Curzon · Dependable computing and fault-tolerant systems · 1993
Cited by 3
David S. Gladstein, Mitchell Wand · Lecture notes in computer science · 1996
Cited by 13
Klaus Didrich · 1997
. The development of correct software is an important task which should not be carried out with the help of tools following different approaches. We propose that full support for correctness proofs should be integrated into the compiler. We outline in this paper how a compiler for a functional language can be extended to support the development of correct software. Specifications, functional programs and proofs are all contained within one compilation unit and can therefore be maintained in close relation to each other. The proof of relations between modules is given special consideration. By managing proof obligations and by deriving standard proofs automatically, the compiler lets the user concentrate on the really difficult proofs. 1 Introduction As software is increasingly used in safety-critical environments, developers have an enhanced interest in the production of correct software. Software engineers, who are used to write large applications and are now persuaded to...
Cited by 0
Adam Chlipala · ACM SIGPLAN Notices · 2015
No abstract available.
Cited by 0
K. Stephenson · 1998
Cited by 0
Nick Benton, Chung-Kil Hur · ACM SIGPLAN Notices · 2009
We define logical relations between the denotational semantics of a simply typed functional language with recursion and the operational behaviour of low-level programs in a variant SECD machine. The relations, which are defined using biorthogonality and stepindexing, capture what it means for a piece of low-level code to implement a mathematical, domain-theoretic function and are used to prove correctness of a simple compiler. The results have been formalized in the Coq proof assistant.
Cited by 16
David Lacey, Neil D. Jones, Eric Van Wyk et al. · Higher-Order and Symbolic Computation · 2004
Cited by 39Open access
Nick Benton, Chung-Kil Hur · 2009
We define logical relations between the denotational semantics of a simply typed functional language with recursion and the operational behaviour of low-level programs in a variant SECD machine. The relations, which are defined using biorthogonality and stepindexing, capture what it means for a piece of low-level code to implement a mathematical, domain-theoretic function and are used to prove correctness of a simple compiler. The results have been formalized in the Coq proof assistant.
Cited by 119
Peter D. Mosses · Lecture notes in computer science · 1980
Cited by 44
Neil D. Jones, David Lacey, Eric van Wyk et al. · Research at the University of Copenhagen (University of Copenhagen) · 2004
compiler correctness, temporal logic, optimisation
Cited by 0
Adam Chlipala · 2009
Abstract. Semantic preservation by compilers for higher-order languages can be verified using simple syntactic methods. At the heart of classic techniques are relations between source-level and target-level values. Unfortunately, these relations are specific to particular compilers, leading to correctness theorems that have nothing to say about linking programs with functions compiled by other compilers or written by hand in the target language. Theorems based on logical relations manage to avoid this problem, but at a cost: standard logical relations do not apply directly to programs with non-termination or impurity, and extensions to handle those features are relatively complicated, compared to the classical compiler verification literature. In this paper, we present a new approach to “open ” compiler correctness theorems that is “syntactic ” in the sense that the core relations do not refer to semantics. Though the technique is much more elementary than previous proposals, it scales up nicely to realistic languages. In particular, untyped and impure programs may be handled simply, while previous work has addressed neither in this context. Our approach is based on the observation that it is an unnecessary handicap to consider proofs as black boxes. We identify some theorem-specific proof skeletons, such that we can define an algebra of nondeterministic compilations and their proofs, and we can compose any two compilations to produce a correct-by-construction result. We have prototyped these ideas with a Coq implementation of multiple CPS translations for an untyped Mini-ML source language with recursive functions, sums, products, mutable references, and exceptions. 1
Cited by 0