NASA
Ames Research Center,
Code IC,
Robust Software Engineering Group,
Ewen Denney,
Bernd Fischer
Proc. Formal Methods (FM 2003), Pisa, Italy,
September 8-14, 2003, Keijiro Araki, Stefano Gnesi, Dino Mandrioli (eds.),
LNCS 2805, pp. 894-913, Springer.
Abstract
Program certification techniques formally show that programs satisfy
certain safety policies. They rely on the correctness of the safety
policy which has to be established externally. In this paper we
investigate an approach to show the correctness of safety policies
which are formulated as a set of Hoare-style inference rules on the
source code level. We develop a framework which is generic with
respect to safety policies and which allows us to establish that
proving the safety of a program statically guarantees dynamic safety,
i.e., that the program never violates the safety property during its
execution. We demonstrate our framework by proving safety policies
for memory access safety and memory read/write limitations to be
sound and complete. Finally, we formulate a set of generic safety
inference rules which serve as the blueprint for the implementation of
a verification condition generator which can be parameterized with
different safety policies, and identify conditions on appropriate
safety policies.
Key words
Program verification, Hoare logic, program safety,
code certification, proof-carrying code
Contents
- Introduction
- Stateless Safety Properties
- Stateful Safety Properties
- Automatic Derivation of Safety Policies
- Related Work
- Conclusions and Future Work
Download complete paper
(106 KBytes, compressed PostScript)
Go to the
home page of the Robust Software Engineering Group
Bernd Fischer /
fisch@email.arc.nasa.gov