spin - Formal correctness prover

Property Value
Distribution NetBSD 7.2
Repository NetBSD i386
Package filename spin-6.4.7.tgz
Package name spin
Package version 6.4.7
Package release -
Package architecture i386
Package type tgz
Category devel
Homepage http://spinroot.com/spin/whatispin.html
License modified-bsd
Maintainer -
Download size 244.25 KB
Installed size 771.81 KB
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.


Package Version Architecture Repository
spin-6.4.7.tgz 6.4.7 amd64 NetBSD
spin - - -


Type URL
Mirror ftp.netbsd.org
Binary Package spin-6.4.7.tgz
Source Package spin

Install Howto

Install spin tgz package:

# pkg_add spin

See Also

Package Description
spiped-1.5.0nb1.tgz Tool for creating symmetrically encrypted and authenticated pipes
spl-1.0pre3nb22.tgz The SPL Programming Language
splay-0.8.2.tgz Audio player/decoder that decodes MPEG Layer I,II,III and WAV files
spleen-1.6.0.tgz Monospaced bitmap fonts
splint-3.1.2nb1.tgz Statically check C programs
splitvt-1.6.6.tgz Run two shells in a split window/terminal
spread-3.17.3nb10.tgz Group communication system providing a number of messaging services
spreadlogd-2.0.0nb22.tgz Daemon to log to file, messages from spread toolkit clients
sptk-3.9.tgz Suite of speech signal processing tools
sql-workbench-124.tgz JDBC-based cross-platform SQL query tool
sqlgrey-1.8.0nb5.tgz Postfix greylisting policy daemon
sqlite-2.8.17nb1.tgz SQL Database Engine in a C Library
sqlite3-3.30.1.tgz SQL Database Engine in a C Library
sqlite3-docs-3.30.1.tgz SQL Database Engine in a C Library (docs package)
sqlite3-tcl-3.30.1.tgz SQL Database Engine in a C Library (TCL extension)