Re: [isabelle] Program verification



Hi Tom,

this might be a bit late, but some such examples are

* my PhD on Java Bytecode Verification
  http://www.cse.unsw.edu.au/~kleing/diss/

* Tobias' and my work on Jinja
  http://www.cse.unsw.edu.au/~kleing/papers/jinja-tr.html

* The NICTA L4.verified project (not yet completed):
  http://nicta.com.au/research/projects/l4.verified

* Xavier Leroy's work on compiler verification:
  http://compcert.inria.fr/

Cheers,
Gerwin

On Tue, 18 Mar 2008, Tom Ridge wrote:
> Dear All,
>
> I am interested in substantial, state-of-the-art examples of program
> verification. "Program" should be interpreted quite widely, e.g. so as
> to include Gonthier's four-colour theorem work, and Harrison's HOL in
> HOL work. "Verification" should also be loosely interpreted, to include
> very weak properties such as e.g. absence of null-pointer dereference,
> as well as strong properties such as functional correctness, liveness etc.
>
> I would be very grateful if people could reply to this message with
> their favourite examples.
>
> I will attempt to set up a wikipedia page with the information so gleaned.
>
> Many thanks
>
> Tom







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.