Re: [isabelle] Isabelle and model checkers

Thanks Sergey, I'll ask Peter about availability of his version.


On Nov 11, 2010, at 3:28 AM, Sergey Tverdyshev wrote:


I heard that Peter Boehm ported it to Isabelle2009 (don't know whether -1 or -2)


On 11 November 2010 12:16, John Matthews <matthews at> wrote:

I'm running Isabelle2009-2 and am looking for external oracles to model checkers like NuSMV, SPIN, Murphi, etc.

So far I found the home page for IHaveIt ( ), but it says it requires Isabelle 2005.

Has anyone ported IHaveIt to Isabelle2009-2, and does anyone know of connections to other model checkers for Isabelle?


Dr.-Ing. Sergey Tverdyshev

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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