PV5 ⊧ SAW: Software Analysis Workbenchextracts an algorithmic spec from source code and uses it on backend verifiers

Application domain/field

• Software verification
• Automated reasoning

Type of tool

Equivalence checker/symbolic execution engine?

Expected input

• Program
• Optional: A specification, consisting of three components:
1. A specification of the initial state before execution of the function
2. A description of how to call the function within that state
3. A specification of the expected final value of the program state.

Format:

• Program: C, Java or Cryptol program or its own SAWScript language.
• Specifications: ?

Internals

Open-source symbolic analysis engine developed by Galois. It uses symbolic execution to reason about a program. It can be used for bug finding and equivalence checking. Uses ABC, Yices, Z3. "SAW was designed with cryptographic implementations in mind, but also supports general purpose imperative programs."