Abstract is missing.
- Frontmatter, Table of Contents, Preface [doi]
- Structuring Interactive Correctness Proofs by Formalizing Coding IdiomsHolger Gast. 1-14 [doi]
- Verification of Dependable Software using SPARK and IsabelleStefan Berghofer. 15-31 [doi]
- Adaptable Value-Set Analysis for Low-Level CodeJörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, Mads Chr. Olesen. 32-43 [doi]
- Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking ToolsAntti Jääskeläinen, Mika Katara, Shmuel Katz, Heikki Virtanen. 44-56 [doi]
- A Tool for the Certification of Sequential Function Chart based System SpecificationsJan Olaf Blech. 57-70 [doi]
- Automatic Derivation of Abstract Semantics From Instruction Set DescriptionsDominique Gückel, Stefan Kowalewski. 71-83 [doi]