Caduceus ( is an academic tool developed at the LRI laboratory at the University of Paris 11. It is based on the Hoare method and offers the possibility of sending the proof obligations that have been generated either to an automatic theorem prover (Simplify or CVS Lite) or to a proof checker (Coq) or to a semiautomatic theorem prover (PVS), each of which is more or less adapted to the program being analyzed. Indeed, the properties generated by the Hoare method reflect what the program is doing, and a given theorem prover might not be the most efficient one when proving all kinds of properties (for instance, some provers might be good for some arithmetic properties and less for others).

Was this article helpful?

0 0
The Ultimate Computer Repair Guide

The Ultimate Computer Repair Guide

Read how to maintain and repair any desktop and laptop computer. This Ebook has articles with photos and videos that show detailed step by step pc repair and maintenance procedures. There are many links to online videos that explain how you can build, maintain, speed up, clean, and repair your computer yourself. Put the money that you were going to pay the PC Tech in your own pocket.

Get My Free Ebook

Post a comment