The Isabelle "ismt" Tactic

Copyright © 2007-2011.

The ismt package allows Isabelle to invoke SRI Inc.’s Yices SMT solver to automatically prove or refute formulas written in the subset of higher order logic that Yices understands. When Yices refutes a formula, theismt package can also convert the Yices-produced counterexample back into a higher order logic formula.

License

The ismt tactic is freely available under a permissive BSD-style license.

Downloading and Installation

The current version of ismt is v1.4. It has been tested to work with Isabelle 2011 and Yices 1.0.29.

  1. Make sure the yices executable (v1.0.29) is in your path.
    • Note that Yices 2.X releases does not work with the ismt tactic yet. (This is because Yices-2.X only accepts SMT-Lib, while the ismt tactic uses Yices’s internal language.)
    • If you don’t want to pollute your path, or if you are maintaining multiple versions of yices on your computer, then set the environment variable ISMT_YICES to point to the executable of the yices 1.0.29 release, with a command like:
        export ISMT_YICES=/usr/local/yices-1.0.29/bin/yices

      Tweaked properly for your shell, OS, yices location, etc.

  2. Put ISMT.thy in a suitable place. (The location of this file is immaterial as long as you can access it. Note that this is the only file you will need to run the ismt tactic.)
  3. At the top-of your own Isabelle theory file where you’d like to use the ismt tactic, simply import the theory ISMT defined in the above file.

Documentation

  • The ismtuser guide.
  • Our AFM’08 (Automated Formal Methods 2008)paper describes the ideas behind ismt.
  • The Isabelle vcg theory (.thy or .pdf), referenced in the above paper.
  • A set of slides on ismt.

Contact

Dylan McNamee