Cubicle 1.0.1 documentation and source

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.

Cubicle model checker

Basic data structures


Variable
Variables of the parameterized domain
Types
Terms, atoms and conjunctions
Cube
Cubes and simplifications
Ast
Abstract syntax tree and transition systems
Node
Node of the search graph
Cubetrie
Trie structure for cubes sets

Backward reachability with approximations and backtracking


Brab
Backward reachability with Approximations and Backtracking
Approx
Approximations and candidates generation
Bwd
Backward reachability with approximation
Pre
Pre-image computation
Safety
Safety checks
Fixpoint
Fixpoint tests with optimizations

Oracles


Oracle
Interface for oracles
Enumerative
Enumerative forward search
Forward
Symbolic forward exploration

Interface with prover


Instantiation
Exhaustive Instantiation features
Prover
Interface with the SMT solver

Frontend


Main
Entry point of Cubicle
Typing
Typing of parameterized systems
Options
Options given on the command line

Miscellaneous


Dot
Generation of graphical search graphs with dot/graphviz
Pretty
Pretty printing functions
Stats
Statistics
Trace
Certificate traces for external verifiers
Util
Utilitaries
Version
Fake_functory
Dummy replacement for Functory library

Common modules


Hashcons
Hash tables for hash consing
Heap
Hstring
Hash-consed strings
Iheap
Timer
Imperative timers for profiling
Vec
Bitv

The Alt-Ergo SMT solver


Smt
The Alt-Ergo zero SMT library
Solver
Solver_types

Copyright (C) 2011-2014, Sylvain Conchon and Alain Mebsout, Universite Paris-Sud 11