SAW (Software Analysis Workbench)

SAW provides analysts with the ability to extract formal models from programs, and analyze them using a variety of automated reasoning tools.

(Initial Release 0.5)

SAW supports analysis of programs written in C, Java™, MATLAB®, and Cryptol, and uses efficient SAT and SMT solvers such as ABC and Yices.

SAW is primarily designed with cryptographic implementations in mind, but also supports general purpose imperative programs.

  • Verification engineers can use SAW to prove that a program implements its specification.
  • Security analysts can have SAW generate models identifying constraints on program control flow to identify inputs that can reach potentially dangerous parts of a program.
  • Cryptographers can have SAW generate models from production cryptographic code for import and use within Cryptol.

Please contact Dylan McNamee if you are interested in obtaining a release of SAW for evaluation purposes.