./devel/spin, Formal correctness prover

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]


Branch: CURRENT, Version: 5.2.5, Package name: spin-5.2.5, Maintainer: agc

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.


Master sites:

SHA1: 274649628c0c8ae3414b863c27a1b8d98a8e9921
RMD160: 8d01f8dd0da8c8013fbb8c6d6e9a8c40b8c5f33f
Filesize: 403.717 KB

Version history: (Expand)


CVS history: (Expand)


   2015-11-03 04:29:40 by Alistair G. Crooks | Files touched by this commit (1995)
Log message:
Add SHA512 digests for distfiles for devel category

Issues found with existing distfiles:
	distfiles/eclipse-sourceBuild-srcIncluded-3.0.1.zip
	distfiles/fortran-utils-1.1.tar.gz
	distfiles/ivykis-0.39.tar.gz
	distfiles/enum-1.11.tar.gz
	distfiles/pvs-3.2-libraries.tgz
	distfiles/pvs-3.2-linux.tgz
	distfiles/pvs-3.2-solaris.tgz
	distfiles/pvs-3.2-system.tgz
No changes made to these distinfo files.

Otherwise, existing SHA1 digests verified and found to be the same on
the machine holding the existing distfiles (morden).  All existing
SHA1 digests retained for now as an audit trail.
   2015-04-18 22:41:10 by Joerg Sonnenberger | Files touched by this commit (1)
Log message:
Not MAKE_JOBS_SAFE.
   2012-10-31 12:19:55 by Aleksej Saushev | Files touched by this commit (1460)
Log message:
Drop superfluous PKG_DESTDIR_SUPPORT, "user-destdir" is default these days.
   2012-06-18 05:42:26 by David A. Holland | Files touched by this commit (1)
Log message:
Needs yacc; seen in the Linux build report.
   2010-10-24 20:54:13 by Alistair G. Crooks | Files touched by this commit (4) | Imported package
Log message:
Initial import of spin version 5.2.5 into the Packages Collection.

	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.

With thanks to the plan9 guys for the nudge