Cubicle is an SMT-based model checker for parameterized systems. It is an open
source software distributed under the Apache license 2.0
http://www.apache.org/licenses/LICENSE-2.0.html.
This is the documentation of the OCaml code generated by ocamldoc. It serves as a reference manual for developers.
| Variable | |
| Types | Terms, atoms and conjunctions |
| Cube | |
| Ast | |
| Node | |
| Cubetrie |
| Brab | Backward reachability with Approximations and Backtracking |
| Approx | |
| Bwd | |
| Pre | |
| Safety | Safety checks |
| Fixpoint | Fixpoint tests with optimizations |
| Oracle | |
| Enumerative | |
| Forward | |
| Murphi | Oracle for BRAB that calls the explicit state model checker Murphi. |
| Instantiation | Exhaustive Instantiation features |
| Prover |
| Main | |
| Typing | |
| Options | Options given on the command line |
| Dot | |
| Pretty | |
| Stats | Statistics |
| Trace | |
| Util | Utilitaries |
| Version | |
| Fake_functory | Dummy replacement for Functory library |
| Hashcons | Hash tables for hash consing |
| Heap | |
| Hstring | Hash-consed strings |
| Iheap | |
| Timer | Imperative timers for profiling |
| Vec | |
| Bitv |
| Smt_sig | A signature for itegrating SMT solvers in Cubicle |
| Smt | A module corresponding to the SMT solver selected by the command line options |
| Alt_ergo | The Alt-Ergo zero SMT library |
| Solver | |
| Solver_types |