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 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.