University of Cincinnati Logo

20-CS-626 - Formal Methods
School of Computing Sciences and Informatics

    Cygwin - unix like shell in Windows
        - Installer 1.
    SAT Solvers
        - SBSAT for unix and windows 2.
        - Minisat for unix
    SMT Solvers
        - Yices for unix, mac, windows
        - Z3 for unix and windows
    Equivalence checkers
        - ABC for linux and windows
    First order logic interactive theorem provers
        - ACL2 for unix, mac, windows
        - ACL2 Sedan (Eclipse-based interface)
        - Emacs for windows - get largest file
        - Isabelle for unix, mac, windows
        - Cryptol, main page
        - Academic Cryptol - email request
        - Sudoku via SAT solver
  1. Run cygwin's "setup" which will ask for packages you want to include in the installation. Click on "Devel" and go to town making sure to check all boxes dealing with gcc, g++, any 'make', any library, and any ncurses package. Then go for dinner.

  2. Get sbsat by following the sbsat link above and clicking on the "complete distributions" link in the "Downloads" section. Fill out the form, preview, and submit. The distribution arrives at your email address. Download the distribution. Assuming you have cygwin installed, open the "All programs" menu to find directories "Cygwin" and "Cygwin-X" click on the latter. Find "XWin Server" and click on that. A nice unix-like shell will appear (at some point). Determine the directory that has sbsat-2.5b-5.tar.gz (probably in something like c:\Users\John\Downloads). In the cygwin shell run this:
      cp c:/Users/John/Downloads/sbsat-2.5b-5.tar.gz .
    (replace the Users/John/Downloads with the actual path to the package and do not neglect the period at the end of the command). Execute the following sequence of commands:
      tar xf sbsat-2.5b-5.tar.gz
      cd sbsat-2.5b-5
      make install
    Now you can run sbsat. Change to your home directory with cd. Run sbsat, for example, like this:
      sbsat -R r yourfile.cnf
Paul Erdos
Ladies on Campus
Oscar Robinson