*Formal Methods*Educational Resources

Formal Methods Education Resources

Tool Pages

Main Page | Courses | Examples | Readings | Position Papers | Instructional Materials | Tools | Jobs | Submit

NOTE: This page references tools suitable for educational purposes (at various levels of the curriculum). Please submit information only on tools which you have actually used in a formal methods-related course. The World Library of Formal Methods provides more general links to tool pages.

Visitors may also be interested in the University of Dortmund's Electronic Tool Integration Platform, an on-line, Java-based, interactive tool repository that lets users experiment with and combine various reasoning tools.

  • ProofBuilder
    Input LanguageTool's own language (first-order or propositional logic)
    Supported TechniquesProof Assistant/Interactive Theorem Proving
    PlatformsAnything that supports Java
    AvailabilityFreely Available, including source

  • SMV
    Input LanguageTool's own language (finite state machine)
    Supported TechniquesModel Checking
    PlatformsLinux, Sparc/Solaris
    AvailabilityFreely Available, including source

  • PVS
    Input LanguageTool's own language (typed higher order logic)
    Supported TechniquesProof Checking, Model Checking
    PlatformsLinux, Sparc/Solaris
    AvailabilityFreely Available, binaries only, under license

  • HOL
    Input LanguageTool's own language (Higher-order logic)
    Supported TechniquesProof Checking
    PlatformsLinux, Alpha, Sparc/Solaris
    AvailabilityFreely Available, including source

  • Murphi
    Input LanguageTool's own language (guarded command language)
    Supported TechniquesModel Checking, Symmetry
    PlatformsLinux, Sparc/Solaris, SGI Indy, HP-UX
    AvailabilityFreely Available, including source

  • SPIN
    Input LanguagePromela
    Supported TechniquesModel Checking, Partial Orders
    PlatformsWindows NT, Windows 95, Linux, Sparc/Solaris
    AvailabilityFreely Available, including source

  • VIS
    Input LanguageVerilog, Tool's own language (blif-mv)
    Supported TechniquesModel Checking, Synthesis
    PlatformsWindows 95, Linux, Alpha, Sparc/Solaris, DEC MIPS, HP Snake
    AvailabilityFreely Available, including source

  • ACL2
    Input LanguageTool's own language (Common Lisp)
    Supported TechniquesHeuristic Theorem Proving, Proof Checking
    PlatformsLinux, Sparc/Solaris
    AvailabilityFreely Available, including source

  • CADP (CAESAR/ALDEBARAN Development Package)
    Input LanguageTool's own language (LOTOS (ISO standard 8807), communicating finite state machines, etc.)
    Supported TechniquesModel Checking
    PlatformsLinux, Sparc/Solaris, Sparc/SunOS
    AvailabilityFree To Universities
    Used in Coursesmany

  • Isabelle/HOL
    Input LanguageTool's own language (higher-order logic)
    Supported TechniquesProof Checking
    PlatformsLinux, Sparc/Solaris
    AvailabilityFreely Available, including source

  • MOCHA
    Input LanguageTool's own language (based on Reactive Modules)
    Supported TechniquesModel Checking, Compositional Reasoning
    PlatformsLinux, Alpha, Sparc/Solaris
    AvailabilityFreely Available, including source
    Used in CoursesComputer-Aided Verification

  • Cadence SMV
    Input LanguageVerilog, Tool's own language (finite-state machine language)
    Supported TechniquesModel Checking, Compositional Reasoning, Symmetry, Abstraction
    PlatformsLinux, Alpha, Sparc/Solaris
    AvailabilityFreely Available, binaries only

  • Triveni
    Input LanguageTool's own language (Java class library)
    Supported TechniquesCompositional Reasoning, Abstraction, Assertions on event sequences via temporal logic
    PlatformsWindows NT, Windows 95, Linux, Alpha, Macintosh, Sparc/Solaris
    AvailabilityFreely Available, including source
    Used in CoursesJava Programming and Concurrency

  • DrScheme
    Input LanguageTool's own language (Scheme)
    Supported Techniquesprogramming environment
    PlatformsWindows NT, Windows 95, Linux, Alpha, Macintosh, Sparc/Solaris, lots of other Unix platforms
    AvailabilityFreely Available, including source
    NotesDrScheme is a pedagogically-motivated programming environment for Scheme. It supports source highlighting of errors, presentation of Scheme via increasingly complex language layers (with additional error-checking at lower levels), a Lisp-style but improved interaction mechanism, robust linguistic extensions for modular, object-oriented and graphical programming, and complete portability across all supported platforms.

  • VeriSoft
    Input LanguageTool's own language (any executable code (C, C++, etc.))
    Supported TechniquesModel Checking
    PlatformsLinux, Sparc/Solaris
    AvailabilityFreely Available, binaries only

  • PEP (Programming Environment based on Petri Nets)
    Input LanguageTool's own language (Parallel programs (B(PN)^2), SDL (Specification Description Language), High-Level and low-level Petri Nets, Process algebra terms (PBC), Parallel finite automata)
    Supported TechniquesModel Checking, Deadlock detection. Structural properties (invariants), Compositional Reasoning, Partial Orders, Symmetry
    PlatformsLinux, Sparc/Solaris, SGI/Irix
    AvailabilityFree To Universities
    Notes PEP has (to my knowledge) been used for courses on Petri nets, process algebras, model checking, verification, parallel systems, SDL and parallel programs. PEP includes interfaces to FC2, INA, SMV and SPIN.

  • VDMTools
    Input LanguageTool's own language (VDM-SL and VDM++)
    Supported TechniquesType checking and Interpretation, Abstraction
    PlatformsWindows NT, Windows 95, Linux, Alpha, Sparc/Solaris
    AvailabilityFree To Universities
    Used in CoursesFormal Specification of Software
    NotesAcademic site licenses available

  • TermiLog
    Supported Techniquestermination analysis, Abstraction
    PlatformsLinux, Sparc/Solaris
    AvailabilityFree To Universities
    Used in CoursesLogic Programming

  • NuSMV
    Input LanguageTool's own language ((finite-state machine language))
    Supported TechniquesModel Checking
    PlatformsLinux, Sparc/Solaris, Intel/Solaris
    AvailabilityFree To Universities
    Used in CoursesModel Checking Tutorial

  • ManTa
    Input LanguageTool's own language (Formal Theory of Abstract Data Types)
    Supported TechniquesHeuristic Theorem Proving, Proof Checking, , Code Synthesis
    PlatformsWindows NT, Windows 95, Linux, Sparc/Solaris, MIPS
    AvailabilityFreely Available, including source
    Used in CoursesVerificación y Desarrollo de Programas

  • SteP (Stanford Temporal Prover)
    Input LanguageTool's own language (fair transition systems)
    Supported TechniquesModel Checking, Deductive Verification, Compositional Reasoning, Abstraction, Hybrid Systems, First-order logic
    PlatformsLinux, Alpha, Sparc/Solaris, SGI
    AvailabilityFreely Available, including source

  • RAISE tools
    Input LanguageTool's own language (specification and design)
    Supported Techniquestype checking; translation
    PlatformsWindows NT, Windows 95, Linux, Sparc/Solaris
    AvailabilityFreely Available, including source
    Used in CoursesFormal Software Specification Using RAISE

  • PV
    Input LanguagePromela
    Supported TechniquesModel Checking, Partial Orders, Selective state caching, memory model verif (prelim)
    PlatformsLinux, Sparc/Solaris
    AvailabilityFreely Available, including source
    Used in CoursesCPSC 6110, Formal Methods in System Design
    NotesSend email to ganesh@cs.utah.edu for problems or questions.

  • Reactis Tester
    Input LanguageTool's own language (Simulink/Stateflow)
    Supported Techniquesautomatic test-suite generation via state exploration
    PlatformsWindows (all varieties), Linux
    AvailabilityCommercial
    NotesEducational discounts available.

  • LTSA
    Input LanguageTool's own language (FSP)
    Supported TechniquesModel Checking, Partial Orders, Synthesis from MSCs
    PlatformsWindows (all varieties), Linux, Macintosh
    AvailabilityFreely Available, binaries only
    Used in CoursesConcurrent Programming

  • Alloy
    Input LanguageTool's own language (Declarative relational logic)
    Supported TechniquesSatisfiability Checking
    PlatformsWindows (all varieties), Linux, Macintosh, Sparc/Solaris
    AvailabilityFreely Available, including source

  • Perfect Developer
    Input LanguageTool's own language (Object oriented)
    Supported TechniquesDerivational/Transformational Reasoning, Heuristic Theorem Proving, Compositional Reasoning, Partial Orders, Abstraction
    PlatformsWindows (all varieties), Linux
    AvailabilityFree to Universities
    Used in Courses Formal Methods (Tony Mullins)
    NotesThe Educational Edition of the tool is free to universities from August 2005. It is also used in courses at other universities, e.g. Portsmouth (UK), Mayneuth (Ireland), TUV (Austria)

    • This site is currently maintained by Kathi Fisler
    Department of Computer Science, Worcester Polytechnic Institute
    Last updated on Monday, 04-Feb-2008 08:02:51 EST
    Acknowledgements