ISSN:
1573-0670
Keywords:
Formal methods
;
fault tolerance
;
case analysis
;
program verification
;
Floyd-Hoare techniques
;
proving claims about systems
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Abstract Proving claims about behavior of software is essential for the qualification of computer-based systems used in the control of nuclear reactors. For this Problem Corner, we select one of the verification conditions for a C program that initializes an array to zero. We add assertions about the initial conditions and state of the program and about the expected behavior of the program in terms of its state. The modeling and specification technique is the inductive assertion technique of Floyd-Hoare. The program with assertions is then transformed by the source-to-source program transformation system TAMPR into a set of separate verification conditions to be proven by the automated reasoning system. Our experience with this program demonstrates the typical automated reasoning problems we have encountered and illustrates how we have approached solutions to the problems.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00243137
Permalink
