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
9 weeks 5 days ago
14 weeks 6 hours ago
15 weeks 4 days ago
15 weeks 4 days ago
18 weeks 2 days ago
22 weeks 6 days ago
22 weeks 6 days ago
23 weeks 2 days ago
23 weeks 2 days ago
26 weeks 1 day ago