Title :
Using formal methods to validate C programs
Author :
Antoine, C. ; Baudin, P. ; Collart, J.M. ; Raguideau, J. ; Trotin, A.
Author_Institution :
Commissariat a l´´Energie Atomique, CEA, Centre d´´Etudes Nucleaires de Saclay, Gif-sur-Yvette, France
Abstract :
Presents the CAVEAT project. The purpose of this project is to develop a tool designed to assist a user in the verification of C programs. Such a verification is required for safety applications in a pragmatic approach. The tool enables a user to verify the global or local properties of these applications. The context in which a property is to be verified is defined in terms of hypotheses. Most of the steps of the verification process, in particular the rewriting steps, are executed automatically. The proof process, however, may be partially interactive, and the interface therefore allows easy communication
Keywords :
interactive systems; program verification; rewriting systems; safety-critical software; software tools; user interfaces; C program validation; CAVEAT project; automatically executed steps; formal methods; global properties; hypotheses; local properties; partially interactive proof process; program verification tool; rewriting steps; safety applications; user interface; Application software; Automatic control; Communication industry; Communication system control; Computer industry; Context; Hardware; Inspection; Legged locomotion; Safety; Software safety; Testing;
Conference_Titel :
Software Reliability Engineering, 1994. Proceedings., 5th International Symposium on
Conference_Location :
Monterey, CA
Print_ISBN :
0-8186-6665-X
DOI :
10.1109/ISSRE.1994.341383
