Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
Institute of Formal Methods in Computer Science

Model-Checking Kit: News


This page will be updated whenever there is something new to report about the Kit; in particular, whenever a new version becomes available.


  • New version 1.4.0 (Linux and source distribution)
  • Support for PNML input language added (implementation by Julian Bart)
  • Added support for Claus Schröter's reachability checker based on complement places (comp-reach)
  • Upgraded Mole to version 1.0.2


  • New version 1.3.1 (all distributions)
  • spin-reach would find deadlocks in addition to the desired target states; fixed


  • New version 1.3.0 (all distributions)
  • LoLA tools added by Karsten Schmidt (see doc/lola/loladoku.txt)
  • spin-reach checker now uses the breadth-first search option (effective only if Spin v4 or higher is used)
  • Most unfolding-based algorithms now use the Mole unfolder (see doc/pep/mole.txt)
  • Test script improved
  • The Linux distribution now requires gcc 3.2 or higher (for the Prod checkers)


  • New version 1.2.0 (all distributions)
  • DSSZ tools added by Alex Tovchigrechko
  • Test script added (see mckit/examples/
  • Mcsmodels upgraded to version 1.7
  • Stopped support for interactive mode (see mckit/src/console.c)
  • Some minor bugfixes


  • New version 1.1.6 (all distributions).
  • Made the Kit compatible with Spin versions above 3.4.


  • New version 1.1.5 (source distribution only).
  • Fixed various compilation problems with new versions of gcc and bison.
  • Web site moved to new location at Stuttgart.
  • Created special binary distribution for gcc 3.2
    (prod didn't run with normal Linux distribution, thanks Oscar Rebeiro for reporting this)



  • New version 1.1.4 (source, Linux and Solaris distribution).
  • Fixed a bug in the driver for Spin when no partitions were available.


  • New version 1.1.3 (source, Linux and Solaris distribution).
  • Fixed a bug in the formula parser for B(PN)2.


  • New version 1.1.2 (source, Linux and Solaris distribution).
  • Support for clp deadlock checker added.
  • Several bugs fixed.


  • New version 1.1.0 (source, Linux and Solaris distribution).
  • New input language IF added (preliminary support).
  • New checker spin-ltl added.


  • New version 1.0.6 (source and Solaris distribution).
  • Some tools (prod, smv) were upgraded to their new versions.
  • Use of ranlib in prod eliminated.


  • There is a new version (1.0.4) available which is compatible with Solaris 2.5.1.
  • Also available for the first time is a Linux version. It has all the functionality of the Solaris version but is missing the apnn-ctl checker.
  • Both new versions are available on the Installation page.


  • Initial release.

Next chapter: How to install the Kit