Paul E. Black, George Becker, and Neil V. Murray, Formal Verification of a Merge-Sort Program with Static Semantics, Proceedings of 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.

Abstract:

    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 DVI (49k), Postscript (114k), or PDF (186k).

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

Updated Wed Jul 10 10:28:05 2002

Go to Black's papers or NIST home page.