[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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and