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 example files.

Contents:

• Getting Started
  • Background
  • Notation
  • Exercises: Initial Setup
  • Troubleshooting / Installation Alternatives
• Specifications and Verification
  • The Code
  • Testing Programs
  • Symbolic Execution
  • Running SAW
• Memory Layout and Pointers
  • Cryptol
• Compositional Verification of Salsa20
  • Salsa20 Verification Overview
  • A Cryptol Specification
  • SAW Specification and Verification
  • Comparing Compositional and Non-compositional Verification
• Extended Exercise: HMAC Maintenance
  • Background: The Updates to the Implementation
  • Exercise: Update the Cryptol Specification
  • Exercise: Update the SAW Specifications
• Example Solution: HMAC Maintenance
  • Updating the Cryptol Specification
  • Updating the SAW Specifications
• Further Reading
  • Specification with Cryptol
  • Verification with SAW
• Glossary

Indices and tables

• Index

• Module Index

• Search Page