PV5 ⊧ SAW: Software Analysis Workbenchextracts an algorithmic spec from source code and uses it on backend verifiers
- Software verification
- Automated reasoning
Type of toolEquivalence checker/symbolic execution engine?
- Optional: A specification, consisting of three components:
- A specification of the initial state before execution of the function
- A description of how to call the function within that state
- A specification of the expected final value of the program state.
- Program: C, Java or Cryptol program or its own SAWScript language.
- Specifications: ?