sci-mathematics/kind2 (gentoo)

Search

Package Information

Description:
Kind 2 is an open-source, multi-engine, SMT-based automatic model checker for safety properties of finite-state or infinite-state synchronous reactive systems expressed as in an extension of the Lustre language. In its basic configuration it takes as input one or more Lustre files annotated with properties to be proven invariant, and outputs for each property either a confirmation or a counterexample, i.e., a sequence inputs that falsifies the property. More advanced features include contract-based compositional verification, proof generation for proven properties, and contract-based test generation.
Homepage:
https://kind2-mc.github.io/kind2/ https://github.com/kind2-mc/kind2/

Versions

Version EAPI Keywords Slot
1.9.0 8 ~amd64 0/1.9.0

Metadata

Description

Maintainers

Upstream

Raw Metadata XML
<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>
    Kind 2 is an open-source, multi-engine, SMT-based automatic model checker
    for safety properties of finite-state or infinite-state synchronous
    reactive systems expressed as in an extension of the Lustre language. In
    its basic configuration it takes as input one or more Lustre files
    annotated with properties to be proven invariant, and outputs for each
    property either a confirmation or a counterexample, i.e., a sequence inputs
    that falsifies the property. More advanced features include contract-based
    compositional verification, proof generation for proven properties, and
    contract-based test generation.
  </longdescription>
	<upstream>
		<bugs-to>https://github.com/kind2-mc/kind2/issues/</bugs-to>
		<remote-id type="github">kind2-mc/kind2</remote-id>
	</upstream>
</pkgmetadata>

Lint Warnings

USE Flags

Flag Description 1.9.0
ocamlopt Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)
test Enable dependencies and/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently)

Manifest

Type File Size Versions
DIST kind2-1.9.0.tar.gz 2009655 bytes 1.9.0
Unmatched Entries
Type File Size