Lambda the Ultimate

Verified Software: Theories, Tools, and Experiments, VSTTE 2006, Workshop proceedings. K. Rustan M. Leino; Wolfram Schulte. August 2006.

The papers are:

• Formalising a High-Performance Microkernel written in Haskell, using Isabelle/HOL.
• Automated Verification of UPC Memory Consistency. UPC is a shared memory extension of C.
• Automated Model-based Verification of Object-Oriented Code, describing ESpec which is a suite of tools that facilitate the testing and verification of Eiffel programs.
• Cross-Verification of JML Tools: An ESC/Java2 Case Study which concludes that the use of JML RAC uncovered desgin flaws that ESC/Java2 was unable to report.
• Static Stability Analysis of Embedded, Autocoded Software.