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.
SAW supports analysis of programs written in C, Java, 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.
The core of the SAW implementation, supporting C, Java, and Cryptol, is freely available under the standard 3-clause BSD license. See the main SAW website for or GitHub project for more details.
