Paul E. Black, George Becker, and Neil V. Murray,
Formal Verification of a Merge-Sort Program with Static Semantics,
The 9th International
Conference on Computing and Information (ICCI'98), Winnipeg,
Manitoba, Canada (June 1998), edited by Kamal Karlapalem, Amin
Y. Noaman, and Ken Barker, pages 271-277.
Proving correctness of programs is a desirable, but not yet
practically solved, problem. Conventional verification techniques do
not scale to larger "real-life" programs. In order to overcome
problems with the semantics of conventional languages, researchers
define subsets of these languages for verification. We take this
approach one step further; rather than defining a subset, we apply a
new theory based on relaxed single-threading to achieve completely
static semantics (i.e. referential transparency) of programs. Our
programs with static semantics have complete control over aliasing,
the correct order dependencies are enforced, and uninitialized
variables are prevented.
Due to the static semantics of these programs, first-order logic can
be used directly to verify them. Using Merge-Sort as an example, we
demonstrate that first-order logic proofs of programs with static
semantics are fully composable and thus scale freely to larger
programs. We also report on our work towards a fully formal,
machine-checked proof. This work is one more step towards
facilitating the design of more easily verified programs.
Get the paper in
Postscript (114k), or
This page's URL is /~black/Papers/icci98.html
Wed Jul 10 10:28:05 2002
by Paul E. Black
Black's papers or
NIST home page.