LLVM/Java Verification with SAW

This tutorial introduces SAW’s LLVM/Java verification capabilities. After completing this tutorial, you will be able to:

• Show that alternative implementations of a function, even across languages, are equivalent

• Use external SMT/SAT solvers to augment SAW’s internal proof system

• Write proofs in SAW compositionally

• Use the SAW REPL to interactively run proofs

You can download the tutorial files.

Contents

• Introduction
• Example: Find First Set
  • Reference Implementation
  • Alternative Implementations
  • Generating LLVM Code
  • Equivalence Proof
  • Cross-Language Proofs
• Using SMT-Lib Solvers
• External SAT Solvers
• Compositional Proofs
  • Compositional Imperative Proofs
• Interactive Interpreter
• Other Examples
  • Java Equivalence Checking
  • AIG Export and Import