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 \(\left|x + \left\lfloor y \right\rfloor \right|\), 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.