.. SAW training materials documentation master file, created by
   sphinx-quickstart on Wed Sep  2 15:21:57 2020.
   You can adapt this file completely to your liking, but it should at least
   contain the root `toctree` directive.

Program Verification with SAW
=============================

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


Indices and tables
==================

* :ref:`genindex`
* :ref:`modindex`
* :ref:`search`