DocumentCode
2176236
Title
Caveat: a tool for software validation
Author
Baudin, P. ; Pacalet, A. ; Raguideau, J. ; Schoen, D. ; Williams, N.
Author_Institution
DTSI-SLA, CEA Saclay, Gif Sur Yvette, France
fYear
2002
fDate
2002
Firstpage
537
Abstract
Caveat is a static analysis tool designed to help verify safety critical software. It operates on ANSI C programs. It was developed by CEA, the French nuclear agency and is used as an operational tool by Airbus-France and EdF, the French electricity company. It is mainly based on Hoare Logic and rewriting of first order logic predicates. The main features of Caveat are property synthesis, navigation facilities, and proof of properties.
Keywords
C language; formal logic; program diagnostics; program verification; safety-critical software; software tools; ANSI C programs; Airbus-France; CEA; Caveat; EdF; French electricity company; French nuclear agency; Hoare Logic; first order logic predicates; rewriting; safety critical software verification; software validation tool; static analysis tool; Application software; Automatic control; Computer crashes; Displays; Joining processes; Logic; Navigation; Software safety; Software tools; Visualization;
fLanguage
English
Publisher
ieee
Conference_Titel
Dependable Systems and Networks, 2002. DSN 2002. Proceedings. International Conference on
Print_ISBN
0-7695-1101-5
Type
conf
DOI
10.1109/DSN.2002.1028953
Filename
1028953
Link To Document