Gentoo Packages

Search

Install

Install this package:

emerge -a sci-mathematics/cubicle

If the package is masked, you can unmask it using the autounmask tool or standard emerge options:

autounmask sci-mathematics/cubicle

Or alternatively:

emerge --autounmask-write -a sci-mathematics/cubicle

Package Information

Description:

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.

Homepage:

https://cubicle.lri.fr/ https://github.com/cubicle-model-checker/cubicle/

License:

Apache-2.0

Versions

Metadata

Description

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

Maintainers

• ML (ml@gentoo.org) - Type: project
• Gentoo Mathematics Project (sci-mathematics@gentoo.org) - Type: project

Upstream

• Bugs: https://github.com/cubicle-model-checker/cubicle/issues/
• Remote IDs:
  • github: cubicle-model-checker/cubicle

<pkgmetadata>
	<maintainer type="project">
		<email>ml@gentoo.org</email>
		<name>ML</name>
	</maintainer>
	<maintainer type="project">
		<email>sci-mathematics@gentoo.org</email>
		<name>Gentoo Mathematics Project</name>
	</maintainer>
	<longdescription>
    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.
  </longdescription>
	<upstream>
		<bugs-to>https://github.com/cubicle-model-checker/cubicle/issues/</bugs-to>
		<remote-id type="github">cubicle-model-checker/cubicle</remote-id>
	</upstream>
</pkgmetadata>

Lint Warnings

• [Warning] USE flag 'emacs' in ebuild 1.2.0-r2 is not documented in metadata.xml
• [Warning] USE flag 'examples' in ebuild 1.2.0-r2 is not documented in metadata.xml
• [Error] Missing md5-cache for ebuild cubicle-1.2.0-r2

USE Flags

Manage flags for this package: euse -i <flag> -p sci-mathematics/cubicle | euse -E <flag> -p sci-mathematics/cubicle | euse -D <flag> -p sci-mathematics/cubicle

Files

• 50cubicle-gentoo.el
• cubicle-1.2.0-which.patch

Manifest