Re: Compiler Correctness

Neelakantan Krishnaswami <neelk@cs.cmu.edu>
7 Feb 2006 15:47:12 -0500

          From comp.compilers

Related articles
Compiler Correctness Pramod.Patangay@gmail.com (pramod) (2006-02-07)
Re: Compiler Correctness find@my.address.elsewhere (Matthias Blume) (2006-02-07)
Re: Compiler Correctness danwang74@gmail.com (Daniel C. Wang) (2006-02-07)
Re: Compiler Correctness neelk@cs.cmu.edu (Neelakantan Krishnaswami) (2006-02-07)
Re: Compiler Correctness neelk@cs.cmu.edu (Neelakantan Krishnaswami) (2006-02-11)
Re: Compiler Correctness danwang74@gmail.com (Daniel C. Wang) (2006-02-11)
Re: Compiler Correctness torbenm@app-1.diku.dk (2006-02-11)
Re: Compiler Correctness henry@spsystems.net (2006-02-11)
Re: Compiler Correctness Sid.Touati@inria.fr (Sid Touati) (2006-02-11)
Re: Compiler Correctness haberg@math.su.se (2006-02-11)
[11 later articles]
| List of all articles for this month |

From: Neelakantan Krishnaswami <neelk@cs.cmu.edu>
Newsgroups: comp.compilers
Date: 7 Feb 2006 15:47:12 -0500
Organization: Carnegie Mellon Univ. -- Computer Science Dept.
References: 06-02-053
Keywords: theory, debug
Posted-Date: 07 Feb 2006 15:47:12 EST

> I have a simple question. Can we prove that a compiler is correct? I
> mean we are given a language with it's syntax and semantics and a
> compiler whose correctness needs to be proved. Is this theoretically
> possible?


Yes, it is. In the POPL 2006 conference proceedings, Xavier Leroy
reported on his efforts implementing a provably-correct compiler for a
subset of C.


The proof is extremely large, however, and in order to ensure the
proof's correctness he had to develop the compiler in a theorem
proving system that verified the correctness of all his proofs.


"Formal certification of a compiler back-end, or: programming a
compiler with a proof assistant"


<http://pauillac.inria.fr/~xleroy/publi/compiler-certif.pdf>
--
Neel Krishnaswami
neelk@cs.cmu.edu
[Interesting paper. I wonder how likely it is that the tools, which
are not small, or the set of axioms have bugs that could affect the
validity of the proof. If it sounds like I'm channelling the famous
1979 proof paper by Perlis et al, it's not surprising since he was my
thesis advisor. -John]



Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.