Reasoning about programs with MPVS The tool MPVS has just been released to help students reason about imperative programs using specifications, loop invariants, and problem decomposition. MPVS does symbolic calculations using constraint programming to check verification conditions. MPVS was developed in Mozart as part of Isabelle Dony's Ph.D. work and is available at: http://sourceforge.net/ under the GNU GPL free software license. Documentation is available in Dony's Ph.D. dissertation at: http://www.info.ucl.ac.be/people/PVR/IsabelleDonyThesis.pdf This work was done under the supervision of Baudouin Le Charlier.
Needless to say, the tool and dissertation are in English :-). Peter Van Roy _________________________________________________________________________________ mozart-users mailing list [email protected] http://www.mozart-oz.org/mailman/listinfo/mozart-users
