Verified Software: Theories, Tools, and Experiments

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.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


See also VSTTE 2005.