Glossary

compositional verification

A verification technique based on the idea that, when proving properties of a given method or function, we can make use of properties we have already proved about its callees.

Cryptol

A specification language for algorithms. Used as the notation for SAWCore in SAWScript.

proof maintenance

The process of keeping verification artifacts, such as specifications and proofs, up to date with changes in a software system over time.

SAWCore

The internal representation for programs in SAW.

SAWScript

The language used to write specifications and describe verification tasks in SAW.

SetupValue

A SAWScript SetupValue can be either a Term or a pointer. Arguments passed to symbolically executed functions must be SetupValues.

specification

A description of what is desired of a program. Specifications can be written in anything from informal English to precise, machine-readable logical formulations.

symbolic execution

The process of running a program where some input values are mathematical expressions (also called a symbolic value) instead of actual values. If the program terminates, the result is a mathematical expression that characterizes its behavior.

symbolic value

A program value that is a mathematical expression, like $∣∣𝑥+⌊𝑦⌋∣∣|x+⌊y⌋|$, instead of concrete bits in memory.

testing

The practice of finding empirical evidence that a program lives up to a specification.

Term

A SAWScript Term is a symbolic value that can only represent values, not pointers. This is in contrast to a SetupValue, which is a superclass of Terms and Pointers. Arguments passed to Cryptol functions must be Terms.

verification

The practice of finding mathematical evidence that a program lives up to a specification.