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.
Most Recent Tech Talk
Title Public Tech Talk: “Toward Robot Autonomy: Tasks, Plans, and Policies”
Date Friday, May 28, 2021
Time 10:00 am
Speaker Mark Moll, Director of Research at PickNik
Location Galois is pleased to host this tech talk via live-stream for the public on May 28, 2021 from 10:00 am to 11:00 am Pacific Time. Send a request to firstname.lastname@example.org to receive meeting information.