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 |