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 SF.net email is sponsored by: Microsoft Defy all challenges. Microsoft(R) Visual Studio 2008. http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
