The Software Analysis Workbench (SAW) is a tool for constructing mathematical models of the semantics of programs, manipulating those models, and proving properties about them, with the aid of external SAT and SMT solvers. The process that SAW uses to accomplish this can be seen as a translation from imperative to functional programs, built on a foundation of symbolic execution. The functional language used to represent program semantics has dependent types, and its implementation includes a rewriter and some simple proof tactics.

This talk has several parts. First, it describes the basic structure and capabilities of SAW, including some examples of widely-used cryptographic code that we have verified with it. Next, it goes on to describe the features of SAW’s intermediate language, including details about how it uses the dependently typed features. Finally, it raises some open questions about what additional uses of dependent types may be useful in the future.