sci-mathematics / cubicle

Model checker for verifying properties of array-based systems

Official package sites : https://cubicle.lri.fr/ · https://github.com/cubicle-model-checker/cubicle/ ·

Summary

Cubicle is an open source model checker for verifying safety properties of array-based 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 model-checks 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 Alt-Ergo; and its parallel implementation relies on the Functory library.

Versions

v1.2.0-r2 :: 0/1.2.0 :: gentoo

Modified
License
Apache-2.0
Keywords
~amd64 ~x86
USE flags
emacs examples

USE flags

General

emacs
Add support for GNU Emacs
examples
Install examples, usually source code

Dependencies

app-editors / emacs : The extensible, customizable, self-documenting real-time display editor

dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles

dev-ml / num : Library for arbitrary-precision integer and rational arithmetic

Runtime Dependencies

app-editors / emacs : The extensible, customizable, self-documenting real-time display editor

dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles

dev-ml / num : Library for arbitrary-precision integer and rational arithmetic

Change logs

Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/cubicle: require ocamlopt
Closes: https://bugs.gentoo.org/895214 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/cubicle: install the provided manual page
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/cubicle: new package; add 1.2.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org>