src/HOL/Modelcheck/README.html
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 15582 7219facb3fd0
permissions -rw-r--r--
Constant "If" is now local
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <!-- $Id$ -->
     4 
     5 <html>
     6 
     7 <head>
     8   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     9   <title>HOL/Modelcheck</title>
    10 </head>
    11 
    12 <body>
    13 
    14 <h2>Invoking Model Checkers in Isabelle/HOL</h2>
    15 
    16 This directory contains the basic setup for integration of some model
    17 checkers in Isabelle/HOL, together with a few basic examples.
    18 
    19 <p>
    20 
    21 Currently, best results are achieved with the <a
    22 href="http://iseran.ira.uka.de/~armin/mucke/"><em>Mucke</em></a> model
    23 checker (version 0.3.5 is known to work).  Theory <tt>MuCalculus</tt>
    24 provides the syntactic and oracle interfaces, while
    25 <tt>MuckeExample1</tt> and <tt>MuckeExample2</tt> demonstrate the
    26 model checker tactic <tt>mc_mucke_tac</tt> in action.  To run the
    27 examples yourself, you only have to point <tt>MUCKE_HOME</tt> in
    28 Isabelle's <tt>etc/settings</tt> to the place where the Mucke binary
    29 has been installed.
    30 
    31 <p>
    32 
    33 In order to support more realistic applications, the <a
    34 href="http://isabelle.in.tum.de/library/HOLCF/IOA/Modelcheck">HOLCF/IOA/Modelcheck</a>
    35 session augments this basic mechanism by further infrastructure for
    36 proofs about I/O automata.  There is a separate <a
    37 href="http://isabelle.in.tum.de/IOA/papers/IOA-modelcheck.pdf">paper</a>
    38 available, describing model checking in Isabelle/IOA in more detail.
    39 
    40 </body>
    41 
    42 </html>