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 Protocol Analysis Using Real Analysis in ACL2
Date Tuesday, November 21, 2023
Time 11:00 am
Speaker Max von Hippel
Location Galois was pleased to host this tech talk via live-stream for the public on November 21, 2023 from 11:00 am to 12:00 pm Pacific Time.
421 SW 6th Avenue, Suite 300
Portland, Oregon 97204 Arlington, VA
901 N Stuart Street, Suite 501
Arlington, Virginia 22203 Minneapolis, MN
111 Third Avenue South, Suite 350
Minneapolis, MN 55401 Dayton, OH
444 E 2nd Street
Dayton, Ohio 45402 email@example.com