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