Abstraction
Shape-value abstraction of assertions
Actions
Rely-guarantee actions
Assertions
Separation logic assertions (symbolic heaps)
Commands
Representation of program commands
Convert
Translate parse tree into the intermediate abstract syntax tree
Exp
Representation of expressions
Genarith
Generation of arithmetic programs
Indpreds
User-defined inductive predicates
Linear
Linearizability
Location
Source file locations (for error messages)
Lockfree
Lock-freedom prover
Misc
Library functions and miscellaneous routines
Parsetree
Abstract syntax tree produced by the parser
Prover
Must-subtraction implementation
Pure
Operations on pure formulae
Symbsimp
Symbolic execution
Tycheck
Type checking & conversion into command language