Verified Software: Theories, Tools, Experiments

1. Front Matter

   PDF

2. Introduction

   1. Verified Software: Theories, Tools, Experiments Vision of a Grand Challenge Project

      • Tony Hoare, Jay Misra

      Pages 1-18

3. Verification Tools

   1. Towards a Worldwide Verification Technology

      • Wolfgang Paul

      Pages 19-25

   2. It Is Time to Mechanize Programming Language Metatheory

      • Benjamin C. Pierce, Peter Sewell, Stephanie Weirich, Steve Zdancewic

      Pages 26-30

   3. Methods and Tools for Formal Software Engineering

      • Zhiming Liu, R. Venkatesh

      Pages 31-41

4. Guaranteeing Correctness

   1. The Verified Software Challenge: A Call for a Holistic Approach to Reliability

      • Thomas Ball

      Pages 42-48

   2. A Mini Challenge: Build a Verifiable Filesystem

      • Rajeev Joshi, Gerard J. Holzmann

      Pages 49-56

   3. A Constructive Approach to Correctness, Exemplified by a Generator for Certified Java Card Applets

      • Alessandro Coglio, Cordell Green

      Pages 57-63

   4. Some Interdisciplinary Observations about Getting the “Right” Specification

      • Cliff B. Jones

      Pages 64-69

5. Software Engineering Aspects

   1. Software Verification and Software Engineering a Practitioner’s Perspective

      • Anthony Hall

      Pages 70-73

   2. Decomposing Verification Around End-User Features

      • Kathi Fisler, Shriram Krishnamurthi

      Pages 74-81

6. Verifying Object-Oriented Programming

   1. Automatic Verification of Strongly Dynamic Software Systems

      • N. Dor, J. Field, D. Gopan, T. Lev-Ami, A. Loginov, R. Manevich et al.

      Pages 82-92

   2. Reasoning about Object Structures Using Ownership

      • Peter Müller

      Pages 93-104

   3. Modular Reasoning in Object-Oriented Programming

      • David A. Naumann

      Pages 105-115

   4. Scalable Specification and Reasoning: Challenges for Program Logic

      • Peter W. O’Hearn

      Pages 116-133

7. Programming Language and Methodology Aspects

   1. Lessons from the JML Project

      • Gary T. Leavens, Curtis Clifton

      Pages 134-143

   2. The Spec# Programming System: Challenges and Directions

      • Mike Barnett, Robert DeLine, Manuel Fähndrich, Bart Jacobs, K. Rustan M. Leino, Wolfram Schulte et al.

      Pages 144-152

   3. Integrating Static Checking and Interactive Verification: Supporting Multiple Theories and Provers in Verification

      • Joseph R. Kiniry, Patrice Chalin, Clément Hurlin

      Pages 153-160

8. Components

   1. Automated Test Generation and Verified Software

      • John Rushby

      Pages 161-172

   2. Dependent Types, Theorem Proving, and Applications for a Verifying Compiler

      • Yves Bertot, Laurent Théry

      Pages 173-181

A Step Towards Verified Software Worries about the reliability of software are as old as software itself; techniques for allaying these worries predate even James King’s 1969 thesis on “A program verifier. ” What gives the whole topic a new urgency is the conjunction of three phenomena: the blitz-like spread of software-rich systems to control ever more facets of our world and our lives; our growing impatience with deficiencies; and the development—proceeding more slowly, alas, than the other two trends—of techniques to ensure and verify software quality. In 2002 Tony Hoare, one of the most distinguished contributors to these advances over the past four decades, came to the conclusion that piecemeal efforts are no longer sufficient and proposed a “Grand Challenge” intended to achieve, over 15 years, the production of a verifying compiler: a tool that while processing programs would also guarantee their adherence to specified properties of correctness, robustness, safety, security and other desirable properties. As Hoare sees it, this endeavor is not a mere research project, as might normally be carried out by one team or a small consortium of teams, but a momentous endeavor, comparable in its scope to the successful mission to send a man to the moon or to the sequencing of the human genome.

• C#
• algorithms
• concurrent systems
• dependability
• distributed systems
• exception handling
• fault tolerance
• formal methods
• logic
• model checking
• programming language
• proving
• software verification
• theorem proving
• verification

Policies and ethics