Model Checking @CMU










Model Checking FTP Instructions

A number of software packages and papers related to formal verification are available by anonymous FTP. They are

  • SMV - a symbolic model checker for CTL [latest revision 2.4.4].
  • CSML and MCB - a language for compositional description of finite state machines and a (non-symbolic) model checker for CTL.
  • A BDD library with extensions for sequential verification.
  • Papers on various related topics.
  • Everything is available on EMC.CS.CMU.EDU (

    Here is an example FTP session:

    % ftp
    Connected to EMC.CS.CMU.EDU.
    220 FTP server (SunOS 4.1) ready.
    Name ( ftp
    331 Guest login ok, send ident as password.
    Password: [type e-mail address as password]
    ftp> bin
    200 Type set to L (byte size 8).
    ftp> cd pub
    250 Directory path set to pub
    ftp> get smv.r2.4.4.tar.Z
    ftp> quit
    221 Goodbye.
    If you are unable to access files by FTP, we can send you email or perhaps a tape. Send requests to

    CMU-SCS Model Checking home page

    Please send any comments and suggestions to  Nishant Sinha - (nishants) at cs dot cmu dot edu.