Email Gateway (Aug 18 2022 at 11:33): Email Gateway (Aug 18 2022 at 11:33):From: Tom Ridge <tjr22@cam.ac.uk>
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
Email Gateway (Aug 18 2022 at 11:40):From: Gerwin Klein <gerwin.klein@nicta.com.au>
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
Last updated: May 03 2024 at 08:18 UTC