Skip to content
The Cubicle model checker
OCaml Coq HTML Makefile M4 Emacs Lisp Other
Branch: master
Clone or download
Pull request Compare This branch is 1 commit ahead of cubicle-model-checker:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
alt-ergo-light
common
doc
emacs
examples
experiments
m4
smt
try-cubicle
util
why
.gitignore
.merlin
.travis.yml
CHANGES
LICENSE
Makefile.in
README.md
TODO
approx.ml
approx.mli
ast.mli
brab.ml
brab.mli
bwd.ml
bwd.mli
configure.in
cube.ml
cube.mli
cubetrie.ml
cubetrie.mli
dot.ml
dot.mli
enumerative.ml
enumerative.mli
fake_functory.ml
fake_functory.mli
fixpoint.ml
fixpoint.mli
forward.ml
forward.mli
instantiation.ml
instantiation.mli
lexer.mll
main.ml
mulexer.mll
muparser.mly
muparser_globals.ml
muparser_globals.mli
murphi.ml
murphi.mli
node.ml
node.mli
options.ml
options.mli
oracle.mli
parser.mly
pre.ml
pre.mli
pretty.ml
pretty.mli
prover.ml
prover.mli
ptree.ml
ptree.mli
safety.ml
safety.mli
stats.ml
stats.mli
tla.ml
tla.mli
trace.ml
trace.mli
trie.ml
trie.mli
types.ml
types.mli
typing.ml
typing.mli
util.ml
util.mli
variable.ml
variable.mli

README.md

Cubicle

Build Status

Cubicle is a tool that combines model checking algorithms and automatic SMT theorem provers with a powerful invariants inference mechanism.

Various examples can be found in the examples subdirectory.

Copyright

Copyright (C) 2011-2017
Sylvain Conchon and Alain Mebsout
Université Paris-Sud 11

This program is distributed underthe Apache Software License version 2.0. See the enclosed file LICENSE.

Installation

To compile Cubicle you will need OCaml version 4.03.0 (or newer) and issue:

./configure
make

then with superuser rights:

make install

Cubicle comes with its own emacs major mode cubicle-mode.el. You should copy this file to your emacs.d directory (or anywhere in your load path) and add the following to your init file (.emacs or emacs.d/init.el):

(setq auto-mode-alist
     (cons '("\\.cub$" . cubicle-mode) auto-mode-alist))
(autoload 'cubicle-mode "cubicle-mode" "Major mode for Cubicle." t)

To add colors to the compilation buffer, also add this:

(require 'ansi-color)
(defun colorize-compilation-buffer ()
   (toggle-read-only)
   (ansi-color-apply-on-region (point-min) (point-max))
   (toggle-read-only))
(add-hook 'compilation-filter-hook 'colorize-compilation-buffer)

Usage

To run Cubicle with its classical backward reachability algorithm on a file file.cub simply do:

cubicle file.cub

To run Cubicle with the BRAB algorithm (with a preliminary forward exploration using 2 processes) on a file file.cub simply do:

cubicle -brab 2 file.cub

You can see the list of Cubcile's options by doing:

cubicle -h

Developers

Documentation for developers is available as ocamldoc comments and can be generated in html format in the doc/ocamldoc directory with:

make doc

A pdf file depicting dependency relations between modules can be generated with:

make archi
You can’t perform that action at this time.