Further Reading

This tutorial is only the beginning. The concepts of specification, verification, and proof maintenance are applicable to a variety of tools, not just SAW, and SAW itself contains many more features than those exhibited here.

Specification with Cryptol

The best source for learning more about Cryptol is the free book Programming Cryptol. Galois maintains this book as Cryptol evolves.

This book is suitable both as a tutorial and as a reference.

Verification with SAW

The SAW tutorial describes small problems, similar in scope to Specifying Memory Layout, but uses a somewhat different set of SAW features. It is a good next step after this document. After that, the SAW manual provides detailed descriptions.