[isabelle] Isabelle/HOL support in Why and Caduceus



Dear Isabelle users,

I have contributed Isabelle/HOL support to the verification tools Why and
Caduceus. Why and Caduceus are software verification tools for a ML-like 
language and the C language  Thus, you can verify programs written in a 
ML-like language and C with Isabelle/HOL. 

Why and Caduceus are developed by Filliatre, Marche and Hubert and you can 
find more about the tools in the following URL.

http://why.lri.fr/index.en.html

The Isabelle/HOL support is already merged in the original distribution and
you can download them from the same URL.

Some examples of verification of C programs can be found in the following URL.
They include bubble sort and reversal of linked lists.

http://www.score.cs.tsukuba.ac.jp/~minamide/caduceus-isabelle/


Yasuhiko Minamide







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.