Overview
Cubicle is an open source model checker for verifying safety properties of arraybased systems. This is a syntactically restricted class of parametrized transition systems with states represented as arrays indexed by an arbitrary number of processes. Cache coherence protocols and mutual exclusion algorithms are typical examples of such systems.
Cubicle modelchecks by a symbolic backward reachability analysis on infinite sets of states represented by specific simple formulas, called cubes. Cubicle is based on ideas introduced by MCMT from which, in addition to revealing the implementation details, it differs in a more friendly input language and a concurrent architecture. Cubicle is written in OCaml. Its SMT solver is a tightly integrated, lightweight and enhanced version of AltErgo; and its parallel implementation relies on the Functory library.
Download
Sources
Cubicle is distributed under
the Apache
licence.
You can download the sources of the latest version of
Cubicle here.
Documentation and source code can be browsed online.
Binaries
Installation instructions
Opam
If you use the package manager opam, the easiest way to install Cubicle is to do: $ opam install cubicle If you don't (want to) use opam, Cubicle can also be installed manually.
Manual installation
To compile Cubicle you will need OCaml version 4.00.0 (or newer) and the Ocaml Functory library version 0.5 (or newer) which can be downloaded here.
Note: You can still compile Cubicle without Functory but you will not be able to use its parallel features.
Uncompress the archive and do:
$ cd cubicle1.1.1
$ ./configure
$ make
then with superuser rigths:
# make install
To run Cubicle with the BRAB algorithm on a
file file.cub simply do:
$ cubicle brab nb file.cub
where nb is the number of different processes that will be
considered for the enumerative forward exploration.
For instance, doing cubicle brab 2
german.cub will first perform an enumeration of the
states of the German protocol for an instance of the system
with only two processes. The BRAB algorithm will then be
initialized and run with the finite model it just constructed.
Publications
 Inférence d'invariants pour le model checking de systèmes paramétrés (in french)
 Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières (in French)
 Invariants for Finite Instances and Beyond
 Vérification de systèmes paramétrés avec Cubicle (in French)

Cubicle: A Parallel SMTbased Model Checker for Parameterized
Systems
Sylvain Conchon, Amit Goel, Sava Krstić, Alain Mebsout, and Fatiha Zaïdi.
PDF BibTeX
In Madhusudan Parthasarathy and Sanjit A. Seshia, editors, CAV 2012: Proceedings of the 24th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, pages 718724, Berkeley, California, USA, July 2012. Springer Verlag.
Experiments
All the following benchmarks have been executed on a 64 bits machine with a quadcore Intel ® Xeon ® processor @ 3.2 GHz and 24 GB of memory. The first four columns give details on the exploration of the finite instance. The last colum reports the total time of BRAB, i.e. the time needed for the forward exploration plus the time used by backward reachability. You can view more details about each result such as inferred invariants and search graphs by clicking on the name of the benchmark.
Forward  Backward  Total time  

# procs  depth lim.  # states  time  # nodes  # inv  # restarts  
Germanish  2  ∞  23  0.01s  4  3  0  0.03s 
Szymanski_at  2  ∞  43  0.02s  31  15  0  0.14s 
Szymanski_na  2  ∞  75  0.02s  38  16  0  0.20s 
German_Baukus  2  ∞  1497  0.02s  43  35  0  0.25s 
German.CTC  2  ∞  1497  0.02s  62  27  0  0.29s 
German_pfs  2  ∞  1737  0.02s  49  35  0  0.34s 
ChandraToueg  2  ∞  148  0.02s  3828 (770 + 1329 + 1729)  5  2  2m17s 
Flash_nodata  2  6  439  0.02s  37  30  0  0.36s 
Flash_buggy  2  6  445  0.02s  228  /  0  2.97s 
Flash  3  14  452,523  8.54s  1047  131  0  5m40s 
Documentation
Description language
Cubicle's input language contains some conventional programming constructs (arrays, enumerated and abstract types etc.). However, since we have designed our language with a particular set of protocols in mind, some of its aspects would need to be improved for describing other classes of algorithms.
In Cubicle, arraybased systems are described by a set of type declarations, a set of array declarations, an initial configuration, and a transition relation given as a set of parameterized transitions.
The language has four builtin data types: integers
(int),
reals (real), boolean
(bool) and the type of process
identifiers (proc). It also supports
userdefined abstract
and enumerated data types. For instance,
type data
type msg = Empty  Req  Ack
defines an abstract type data, and an enumeration type
msg with the three given values.
The state of a system is described by a set of global variables and
arrays indexed by process identifiers. Thus,
var Memory : data
var Counter : int
array Channel[proc] : msg
describe the state consisting of two global
variables Memory
and Counter, respectively of
type data and
int, and an
array Channel containing values of
type msg.
The initial state is defined by a universal conjunction of
literals characterizing the values for some variables and arrays. For
example, the configuration
where Counter initially equals to
1 and Channel[z]
contains the value Empty
for any process z is expressed by:
init (z) { Counter = 1 && Channel[z] = Empty }
The execution of a parameterized system is defined by a set of
guarded transitions and consists of an infinite loop which
nondeterministically triggers at each iteration a transition whose
guard is true and whose action is to update state variables. Each
transition can take one or several process identifiers as arguments. A
guard is a conjunction of literals (equations, disequations or
inequations) and universal formulas. These formulas must be in
disjunctive normal form and are universally quantified by processes
different from the transition's arguments. Assignments of variables
can possibly be nondeterministic (denoted by := .). Arrays
updates are realized through a casedefined construct where each
condition is expressed as a conjunction of literals and the default
case is denoted by _.
transition send_req(i)
requires
{ Channel[i] = Empty && Counter < 10 &&
forall_other j. (j < i  Channel[j] <> Req) }
{
Counter := Counter + 1 ;
Memory := . ;
Channel[j] := case
 j = i : Req
 _ : Channel[j];
}
The safety property to be verified is expressed in its negated form as
a cube, existentially quantified by distinct processes, and
characterizes unsafe states. The user also has an option to
specify invariants of the system. For instance, the following formula
expresses that a state is unsafe when there exists two distinct
processes z1
and z2 such
that Channel
contains Req for both.
unsafe (z1 z2)
{ Channel[z1] = Req && Channel[z2] = Req }
Options
Cubicle can be run with different options that are shown below:
version  Print the version number on stdout and exit. 
quiet  Prevent Cubicle from printing the search trace while it performs backward reachability. 
depth n  Limit the depth of the search tree to n at maximum. If this limit si excedeed Cubicle will print reach bound on stderr. This value is set to 100 by default. 
nodes n  Limit the number of nodes to explore to n at maximum. If this limit si excedeed Cubicle will print reach bound on stderr. This value is set to 100000 by default. 
search s  Set the search strategy to s. s can be either breadthfirst search (bfs) or depthfirst search (dfs) or a variant of DFS (dfsl, dfsh, dfshl). By default, Cubicle explores the search space breadthfirst (bfs). 
debug  When this flag is present, Cubicle will output cubes that were computed during the pre, and that are being explored. 
v  When this flag is present together with debug, Cubicle will output the result of the pre. 
profiling  Tells cubicle to output profiling informations at the end of the search. Such as the time that was spent in computing preimages, in the fixpoint checks, in computing relevant permutations, in applying substitutions, in the solver, etc. 
postpone n  Select the strategy to postpone
nodes. Values for n can be:

nodelete  Deactivate a posteriori deletion of nodes that become subsumed. 
j n  Run Cubicle in parallel on n cores. This option can only be used with the search strategy set to BFS. (Do not use in conjunction with brab.) 
h, help  Display a message with usage and the list of options. 
Options relevant to BRAB
brab n  Runs BRAB with a forward exploration with n processes. 
forwarddepth d_{max}  Limits the forward exploration to states at depth d_{max} at maximum. 
onlyforward  Stops after forward exploration. 
candheur nb  Select canditate invariants heuristic with nb (by default nb is the argument of brab). 
v  Increases verbosity of debugging information. 
dot level  Displays search graph (dot must be installed) with detail level level (between 0 and 5). 
When running, Cubicle will produce traces on stdout for each
node that is explored. For example, a node with the following
trace
inv_2(#2) > gnt_shared(#1) > unsafe
will represent states that can reach the unsafe state by
first applying transition inv_2 in
process #2 and then applying
transition gnt_shared in
process #1.
If a system is proved unsafe, Cubicle will say so and output a couterexample trace from the inital state to the unsafe state in the same format.
Changelog
1.1.1 20170613 NEW FEATURES * Option noqe to disable elimination of constants BUG FIXES * Parsing floats and negative reals/integers * Fix too broad overapproximation with nondeterministic updates * Fix type bool is now an enumerative data type 1.1 20160317 NEW FEATURES * Murphi (external tool) as an oracle for performing enumerative forward (Experimental) * Macros for predicates/formulas (Experimental) * Symmetry reduction by normalization in enumerative forward. Can be disabled with forwardnosym. IMPROVEMENTS * Report solver errors * Indentation in Why3 certificates * Stop forward exploration with CtrlC and continue with backward * Sort transitions to not depend on order BUG FIXES * Renaming bug in forward * Certificates: reals/constants and user supplied invariants * Various fixes in reporting of spurious traces * Add user supplied invariants in initial formula * Various fixes in arithmetic 1.0.2 20150209 BUG FIXES * Create correct actions for preservation of values in Enumerative * Fix incorrect computation of subtypes in presence of nondeterministic updates * Fix replaying of error traces with nondeterministic updates 1.0.1 20141105 NEW FEATURES * Certificates in Why3 format (Experimental) * Case constructs for updating global variables * Disjunctions in transitions' requirements (only dnf for now) * Option candheur to (partially) control heuristic for candidate invarariants extraction IMPROVEMENTS * Simplifications in initial formula BUG FIXES * Ignore signal USR1 in Windows because it does not exist 1.0 20140721 NEW FEATURES * New modular architecture with cleaner and more efficient operations * Code documentation with ocamldoc * Use of ? instead of . for nondeterministic assignments (conservative extension: the old syntax is still possible) IMPROVEMENTS * More efficient forward (with GC parameters) * Faster filter when a lot of candidates are not suitable * New options for controlling candidates generation * More options for dot search graphs and color by exploration time * More efficient tries (less allocation) BUG FIXES * Report typing errors (at transition level) * Relevant permutations for multidimensional arrays 0.6 20140127 NEW FEATURES * Refine universal guards by symbolic forward replay to prevent spurious traces when using BRAB (experimental) * Certificates (of inductiveness) generation for AltErgo and Why3 * Specify max number of processes with keyword : number_procs * Show spurious error traces IMPROVEMENTS * Use generic parameterized hash functions: faster with OCaml >= 4.00 * Do not add spurious nodes in visited * More efficient computation of preimages * Use ocamlfind for configure BUG FIXES * Arithmetic simplifications 0.5 20130904 NEW FEATURES * BRAB algorithm on top of classical backward reachability * Generation of search graph in dot (graphviz) format thanks to unsat cores * Allow non deterministic updates of variables of type other than proc * Enumerative statefull forward exploration * Multidimensionnal arrays IMPROVEMENTS * Copy of cyclic datastructures * Only use features of the SMT solver that are necessary: congruence closureand arith are deactivated when not needed * SAT solver (altergo zero): delay case split once a full propositional model is found * Tries for maintaining set of visited nodes (cubes) * Memoization of (SMT) formula construction * Check other candidates on faulty traces BUG FIXES * SAT solver (altergo zero): Raise sat if full model to avoid vec assert * Raise error on duplicate updates 0.2.5 20120412 NEW FEATURES * Complete error traces BUG FIXES * Fix bug in initial formula instantiation with global variables 0.2.4 20120411 NEW FEATURES * Syntactic sugar for simple array updates (A[i] := v) BUG FIXES * Pre with correct number of arguments 0.2.3 20120402 BUG FIXES * Computation of pre for terms of the form A[G] 0.2.2 20120323 NEW FEATURES * Multiple unsafe properties * Allow terms of the form A[G] where A is an array and G is a global variable 0.2.1 20120125 IMPROVEMENTS * Approximations in arithmetic simplifications 0.2 20120123 * First public release of Cubicle
Examples
Below is an example of a simple mutal exclustion algorithm
Mutex:
var Turn : proc
array Want[proc] : bool
array Crit[proc] : bool
init (z) {
Want[z] = False && Crit[z] = False
}
unsafe (x y) {
Crit[x] = True && Crit[y] = True
}
transition req (i)
requires { Want[i] = False }
{
Want[j] := case
 i = j : True
 _ : Want[j]
}
transition enter (i)
requires {
Want[i] = True
&& Crit[i] = False
&& Turn = i }
{
Crit[j] := case
 i = j : True
 _ : Crit[j]
}
transition exit (i)
requires { Crit[i] = True }
{
Turn := . ;
Crit[j] := case
 i = j : False
 _ : Crit[j] ;
Want[j] := case
 i = j : False
 _ : Want[j]
}
Contact
You can contact us at our respective email addresses.