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

Application domain/field

Type of tool

Equivalence checker/symbolic execution engine?

Expected input



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."
C Java


Related papers

https://doi.org/10.1007/978-3-319-48869-1_5 (VSTTE 2016)

Last publication date

8 November 2016

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.