SAW Documentation
LLVM/Java Verification with SAW
Rust Verification with SAW
SAW User Manual
Overview
Structure of SAWScript
Invoking SAW
Cryptol and its Role in SAW
Loading Code
Analyzing Hardware Circuits using Yosys
Creating Symbolic Variables
Symbolic Execution
Symbolic Termination
The Term Type
Specification-Based Verification
Bisimulation Prover
Transforming Term Values
Proofs about Terms
Extraction to the Coq theorem prover
Formal Deprecation Process
Appendices
Glossary
Command Reference
REPL Reference
Deprecated Items
SAWScript Language Reference
SAW Documentation
SAW User Manual
Appendices
SAWScript Language Reference
View page source
SAWScript Language Reference
Warning
This section is under construction!
Versions
v: master