Re: [isabelle] Isabelle and model checkers



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

-john

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

John,

I heard that Peter Boehm ported it to Isabelle2009 (don't know whether -1 or -2)
 http://www.comlab.ox.ac.uk/publications/publication3661-abstract.html

Best,
Sergey

On 11 November 2010 12:16, John Matthews <matthews at galois.com> wrote:
Hello,

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 (http://www-wjp.cs.uni-saarland.de/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?

Thanks,
-john




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