Skip to main content
SpringerLink
Log in

Verified Software: Theories, Tools, Experiments

First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions

  • Book
  • © 2008

Overview

Editors:
  1. Bertrand Meyer
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Jim Woodcock
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 4171)

Part of the book sub series: Programming and Software Engineering (LNPSE)

Included in the following conference series:

Conference proceedings info: VSTTE 2005.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (59 chapters)

  1. Front Matter

    Download chapter PDF

  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

  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
Back to top

Keywords

About this book

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.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation