Automatic Program Verification III: A Methodology for Verifying Programs. AIM-256
Abstract/Contents
- Abstract
The paper investigates methods for applying an on-line interactive
verification system designed to prove properties of PASCAL programs.
The methodology is intended to provide techniques for developing a
debugged and verified version starting from a program, that - is
possibly unfinished in some respects, - may not satisfy the required
specifications,i.e., may contain bugs, - may be incompletely
documented in the sense that the assertions provided by the
programmer are not sufficient for proving correctness. It deals with
programs that may be written in non-standard ways, e.g., permits user
defined data structures.The methodology involves - techniques for describing data structures,
type constraints, and properties of programs and subprograms (i.e.
lower level procedures); - the use of (abstract) data types in
structuring programs and proofs. - interactive application of a
verification condition generator, an algebraic simplifier and a
theorem-prover;Within each unit (i.e. segment of a problem), the interactive use is
aimed at reducing verification conditions to manageable proportions
so that the non-trivial factors may be analysed. Analysis of
verification conditions attempts to localize errors in the program
logic, to extend assertions inside the program, to spotlight
additional assumptions on program subfunctions beyond those already
specified by the programmer, and to generate appropriate lemmas and
assumptions that allow a verification to be completed. Methods for
structuring correctness proofs are discussed.A detailed case study of a pattern matching algorithm illustrating
the various aspects of the methodology (including the role played by
the user) is given.
Description
Type of resource | text |
---|---|
Form | memorandums |
Extent | 1 text file |
Place | Stanford (Calif.) |
Date created | December 1974 |
Language | English |
Digital origin | reformatted digital |
Creators/Contributors
Author | von Henke, Friedrich W. | |
---|---|---|
Author | Luckham, David C. |
Subjects
Subject | Stanford Artificial Intelligence Laboratory |
---|---|
Subject | Memo (Stanford Artificial Intelligence Laboratory) |
Subject | Artificial intelligence |
Genre | Memorandums |
Bibliographic information
Finding Aid | |
---|---|
Memo | AIM-256 |
Location | https://purl.stanford.edu/zx345dy4371 |
Location | SC1041 |
Repository | Stanford University. Libraries. Department of Special Collections and University Archives |
Access conditions
- Use and reproduction
- The materials are open for research use and may be used freely for non-commercial purposes with an attribution. For commercial permission requests, please contact the Stanford University Archives (universityarchives@stanford.edu).
- Copyright
- Copyright © The Board of Trustees of the Leland Stanford Junior University. All rights reserved.
Collection
Stanford Artificial Intelligence Laboratory records, 1963-2009
View other items in this collection in SearchWorksAlso listed in
Loading usage metrics...