Integrated theorem prover in compiler

Murali Sitaraman <MSITARA@clemson.edu>
Fri, 16 Oct 2009 16:55:01 -0400

          From comp.compilers

Related articles
Integrated theorem prover in compiler cdegouw@gmail.com (- -) (2009-08-19)
Re: Integrated theorem prover in compiler bmd@cs.kuleuven.be (bart demoen) (2009-08-19)
Re: Integrated theorem prover in compiler walter@bytecraft.com (Walter Banks) (2009-08-19)
Re: Integrated theorem prover in compiler pertti.kellomaki@tut.fi (Pertti Kellomaki) (2009-08-20)
Re: Integrated theorem prover in compiler torbenm@pc-003.diku.dk (2009-08-20)
Re: Integrated theorem prover in compiler gneuner2@comcast.net (George Neuner) (2009-08-20)
Re: Integrated theorem prover in compiler bobduff@shell01.TheWorld.com (Robert A Duff) (2009-08-20)
Integrated theorem prover in compiler MSITARA@clemson.edu (Murali Sitaraman) (2009-10-16)
| List of all articles for this month |

From: Murali Sitaraman <MSITARA@clemson.edu>
Newsgroups: comp.compilers
Date: Fri, 16 Oct 2009 16:55:01 -0400
Organization: Compilers Central
References: 09-08-030
Keywords: theory
Posted-Date: 18 Oct 2009 17:04:10 EDT

One of my colleagues brought this message to my attention. Those
interested in this topic might be interested in RESOLVE. RESOLVE is
an integrated specification and implementation language that lets you
specify, develop, compile and verify the kinds of generic components
you may write in Java, C#, or C++. It is in some sense a response to
Tony Hoare's grand challenge; see his article in October CACM for a
short summary.


RESOLVE is a sourceforge project. Please see
www.cs.clemson.edu/~resolve for a current version of RESOLVE verifier
and compiler (actually, a translator to Java). I expect that a web
version will be posted at the site for trying out the
compiler/verifier within the next week.


RESOLVE is very much a research effort involving Clemson, Ohio State,
and several other institutions. While the group has made decent
progress, plenty of research questions remain (including specification
and analysis of memory usage constraints). The technical reports at
the site have details. See the ones on Push-button Verification and
Verification Vision, for example.


Thanks for any feedback.


Three points wrt follow-up messages to the original posting:


Any mathematical theorem used by the RESOLVE verifier must have a
mechanically-derived or mechanically-checkable proof (in other words,
theorems are not accepted based on "social processes.")


A verifier merely proves that code is correct wrt stated
specifications, so as was rightly pointed out in a follow-up, there is
still the separate task of checking that the specifications do indeed
capture requirements. Also, testing will be necessary to validate
code against customer requirements.


RESOLVE language and verifier are designed to verify software one
component at a time in a modular fashion.


Murali
------
> In Eiffel it is possible to specify a function precondition,
> postcondition and loop invariants, but these are not statically
> checked by the compiler (at compile-time), but instead run-time. An
> exception is thrown if any assertion is violated, but of course this
> only shows that for _that particular execution_ no assertion was
> violated. I could not find any compiler that proofs correctness of a
> given function at compile-time. ...


Post a followup to this message

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