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
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;
Conference_Titel :
Dependable Systems and Networks, 2002. DSN 2002. Proceedings. International Conference on
Print_ISBN :
0-7695-1101-5
DOI :
10.1109/DSN.2002.1028953
