Paul E. Black and Phillip J. Windley, Inference Rules for Programming Languages with Side Effects in Expressions, 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.

Abstract:

    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 DVI (34k), Postscript (128k), or PDF (188k).

This page's URL is /~black/Papers/hol96.html

Updated Wed Jul 10 10:27:04 2002

Go to Black's papers or NIST home page.