Manual

• Overview
• Invoking SAW
• Structure of SAWScript
  • Syntax
  • Basic Types and Values
  • Basic Expression Forms
  • Other Basic Functions
• The Term Type
• Cryptol and its Role in SAW
• Transforming Term Values
  • Rewriting
  • Folding and Unfolding
  • Other Built-in Transformation and Inspection Functions
  • Loading and Storing Terms
• Proofs about Terms
  • Automated Tactics
  • Proof Script Diagnostics
  • Rewriting in Proof Scripts
  • Other Transformations
  • Other External Provers
  • Offline Provers
  • Miscellaneous Tactics
  • Proof Failure and Satisfying Assignments
  • AIG Values and Proofs
• Symbolic Execution
• Symbolic Termination
• Loading Code
• Direct Extraction
• Creating Symbolic Variables
• Monolithic Symbolic Execution
  • Examples
  • Limitations
• Specification-Based Verification
  • Configuring the Initial State
  • Specifying the Final State
  • Running Proofs
• Compositional Verification
• Controlling Symbolic Execution
• LLVM Verification Using Crucible
  • Running a Verification
  • Structure of a Specification
  • Creating Fresh Variables
  • The SetupValue Type
  • Executing
  • Return Values
  • A First Simple Example
  • Specifying Heap Layout
  • Specifying Heap Values
  • Working with Compound Types
  • Preconditions and Postconditions
  • A Heap-Based Example