devel/spin - The NetBSD Packages Collection

Tool for formal verification of multi-threaded software applications

To verify a design, a formal model is built using PROMELA, Spin's
input language.  PROMELA is a non-deterministic language, loosely
based on Dijkstra's guarded command language notation and borrowing
the notation for I/O operations from Hoare's CSP language.

Spin can be used in four main modes:

1.  as a simulator, allowing for rapid prototyping with a random,
guided, or interactive simulations

2.  as an exhaustive verifier, capable of rigorously proving the
validity of user specified correctness requirements (using partial
order reduction theory to optimize the search)

3.  as proof approximation system that can validate even very large
system models with maximal coverage of the state space.

4.  as a driver for swarm verification (a new form of swarm
computing), which can make optimal use of large numbers of available
compute cores to leverage parallelism and search diversification
techniques, which increases the chance of locating defects in very
large verification models.

Build dependencies

pkgtools/mktools pkgtools/cwrappers

Runtime dependencies

(none)

Binary packages

OSArchitectureVersion
NetBSD 10.0aarch64spin-6.5.2.tgz
NetBSD 10.0aarch64spin-6.4.7.tgz
NetBSD 10.0aarch64spin-6.5.2.tgz
NetBSD 10.0aarch64ebspin-6.5.2.tgz
NetBSD 10.0aarch64ebspin-6.5.2.tgz
NetBSD 10.0alphaspin-6.5.2.tgz
NetBSD 10.0earmv6hfspin-6.5.2.tgz
NetBSD 10.0earmv6hfspin-6.4.7.tgz
NetBSD 10.0earmv6hfspin-6.5.2.tgz
NetBSD 10.0earmv7hfspin-6.5.2.tgz
NetBSD 10.0earmv7hfspin-6.4.7.tgz
NetBSD 10.0earmv7hfspin-6.5.2.tgz
NetBSD 10.0i386spin-6.5.2.tgz
NetBSD 10.0i386spin-6.5.2.tgz
NetBSD 10.0powerpcspin-6.5.2.tgz
NetBSD 10.0vaxspin-6.5.2.tgz
NetBSD 10.0x86_64spin-6.5.2.tgz
NetBSD 10.0_BETAx86_64spin-6.5.2.tgz
NetBSD 8.0i386spin-6.5.2.tgz
NetBSD 8.0i386spin-6.4.7.tgz
NetBSD 8.0i386spin-6.5.2.tgz
NetBSD 8.0powerpcspin-6.4.7.tgz
NetBSD 8.0powerpcspin-6.5.2.tgz
NetBSD 8.0powerpcspin-6.5.2.tgz
NetBSD 8.0x86_64spin-6.5.2.tgz
NetBSD 8.0x86_64spin-6.4.7.tgz
NetBSD 8.0x86_64spin-6.5.2.tgz
NetBSD 9.0aarch64spin-6.5.2.tgz
NetBSD 9.0aarch64spin-6.4.7.tgz
NetBSD 9.0aarch64spin-6.5.2.tgz
NetBSD 9.0alphaspin-6.4.7.tgz
NetBSD 9.0alphaspin-6.5.2.tgz
NetBSD 9.0earmspin-6.4.7.tgz
NetBSD 9.0earmv6hfspin-6.5.2.tgz
NetBSD 9.0earmv6hfspin-6.4.7.tgz
NetBSD 9.0earmv6hfspin-6.5.2.tgz
NetBSD 9.0earmv7hfspin-6.5.2.tgz
NetBSD 9.0earmv7hfspin-6.4.7.tgz
NetBSD 9.0earmv7hfspin-6.5.2.tgz
NetBSD 9.0i386spin-6.5.2.tgz
NetBSD 9.0i386spin-6.5.2.tgz
NetBSD 9.0m68kspin-6.4.7.tgz
NetBSD 9.0mips64ebspin-6.4.7.tgz
NetBSD 9.0powerpcspin-6.5.2.tgz
NetBSD 9.0powerpcspin-6.4.7.tgz
NetBSD 9.0powerpcspin-6.5.2.tgz
NetBSD 9.0sh3elspin-6.4.7.tgz
NetBSD 9.0sparc64spin-6.4.7.tgz
NetBSD 9.0sparcspin-6.4.7.tgz
NetBSD 9.0vaxspin-6.4.7.tgz
NetBSD 9.0x86_64spin-6.5.2.tgz
NetBSD 9.0x86_64spin-6.5.2.tgz
NetBSD 9.3x86_64spin-6.5.2.tgz
NetBSD 9.3x86_64spin-6.5.2.tgz

Binary packages can be installed with the high-level tool pkgin (which can be installed with pkg_add) or pkg_add(1) (installed by default). The NetBSD packages collection is also designed to permit easy installation from source.

Available build options

(none)

Known vulnerabilities

The pkg_admin audit command locates any installed package which has been mentioned in security advisories as having vulnerabilities.

Please note the vulnerabilities database might not be fully accurate, and not every bug is exploitable with every configuration.


Problem reports, updates or suggestions for this package should be reported with send-pr.