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.
Recent comments
11 weeks 1 day ago
15 weeks 3 days ago
17 weeks 11 hours ago
17 weeks 11 hours ago
19 weeks 5 days ago
24 weeks 2 days ago
24 weeks 2 days ago
24 weeks 5 days ago
24 weeks 5 days ago
27 weeks 4 days ago