Cubicle 1.1.2 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
Types

Terms, atoms and conjunctions

Cube
Ast
Node
Cubetrie

Backward reachability with approximations and backtracking

Brab

Backward reachability with Approximations and Backtracking

Approx
Bwd
Pre
Safety

Safety checks

Fixpoint

Fixpoint tests with optimizations

Oracles

Oracle
Enumerative
Forward
Murphi

Oracle for BRAB that calls the explicit state model checker Murphi.

Interface with prover

Instantiation

Exhaustive Instantiation features

Prover

Frontend

Main
Typing
Options

Options given on the command line

Miscellaneous

Dot
Pretty
Stats

Statistics

Trace
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_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

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