SAW, the Software Analysis Workbench, is a tool for program verification. This example-driven tutorial demonstrates how to use SAW for common tasks and how to integrate it into the software development lifecycle. The tutorial makes use of several :download:`example files </examples.tar.gz>`.
.. toctree:: :maxdepth: 2 :caption: Contents: Getting Started <GettingStarted> Specifications and Verification <IntroToSAW> Memory Layout and Pointers <Pointers> Compositional Verification of Salsa20 <Salsa20> Extended Exercise: HMAC Maintenance <HMACProblem> Example Solution: HMAC Maintenance <HMACSolution> Further Reading <Further> Glossary