A program verification system based on Oz

We present an imperative program verification system that exploits many powerful aspects of Oz. Our verification system supports an expressive assertion language for writing specifications and loop invariants. It is able to prove the correctness of elaborated imperative programs consisting of several subproblems that are checked independently. We illustrate the functionalities of our system on a few non trivial examples. Then, we explain that, using Oz constraint programming and other convenient programming mechanisms of Oz, the implementation of the system is straightforward. We also provide information about the efficiency of our implementation.