Index of types
Index of exceptions
Index of values
Index of modules
Index of module types


Model
This module defines the input interface of the model-checking engine, which is given by the signature S below.
ModelChecker
Model Checker.
TraceChecker
Trace Checker.
TraceCheckerUtil
Common utility functor for trace-checking engines.
Option
This module manages global options and performs command-line processing.
ScmWrapper
SCM Model Wrapper.
Armc
Cegar
LazyAbstraction
Lazy Abstraction Refinement Tree.
StaticAnalyzer
ReachabilityTree
Reachability Trees.
Validator
Inductive invariant checking and path feasibility.
APInv
UPInv
Control