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.

xref

See also VSTTE 2005.