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 |