[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.


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.


Yasuhiko Minamide

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