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.
Binaries
 Linux x86_64 (Glibc ≥ 2.13)
 Linux x86 (Glibc ≥ 2.15)
 Win32 x86 (MinGW)
 Mac OS X x86 (≥ 10.5.8)
Installation instructions
To compile Cubicle you will need OCaml version 3.11 (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 cubicle0.5
$ ./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
 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 
Manual
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. 
v  Increases verbosity of debugging information. 
dot  Displays search graph (dot must be
installed). Use in conjuction with v to increase details of the graph (maximum detail at v v v). 
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.
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.