Paul E. Black and Phillip J. Windley,
Inference Rules for Programming Languages with Side Effects in
Theorem Proving in Higher Order Logics: 9th International Conference
(TPHOLs '96), Turku, Finland (August 1996),
edited by Joakim von Wright, Jim Grundy, and John Harrison,
Springer-Verlag, Berlin, Germany, 1996, pages 51-60.
Much of the work on verifying software
has been done on simple, often artificial, languages or subsets of
existing languages to avoid difficult details. In trying to
verify a secure application written in C, we have encountered and
overcome some semantically complicated uses of the language.
We present inference rules for assignment
statements with pre- and post-evaluation side effects
and while loops with arbitrary
pre-evaluation side effects in the test expression. We also
discuss the need to abstract the semantics of program
functions and present an inference rule for abstraction.
Get the paper in
Postscript (128k), or
This page's URL is /~black/Papers/hol96.html
Wed Jul 10 10:27:04 2002
by Paul E. Black
Black's papers or
NIST home page.