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
7 weeks 1 day ago
7 weeks 3 days ago
7 weeks 4 days ago
14 weeks 4 days ago
20 weeks 2 days ago
20 weeks 3 days ago
21 weeks 2 days ago
24 weeks 18 hours ago
25 weeks 3 days ago
25 weeks 4 days ago