./devel/spin, Formal correctness prover

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


Branch: CURRENT, Version: 6.4.7, Package name: spin-6.4.7, 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.


Required to build:
[pkgtools/cwrappers]

Master sites:

SHA1: 307ae8ce800dd62520ea118f144a806c14cdf4a5
RMD160: 2b07b9c25fcd7f934dc86241069c39e3dfc426ee
Filesize: 503.058 KB

Version history: (Expand)


CVS history: (Expand)


   2017-12-10 15:02:33 by Adam Ciarcinski | Files touched by this commit (1)
Log message:
removed spin-license

On 30 December 2015 Alcatel-Lucent (the company that inherited Bell Laboratories \ 
from AT&T in the trivestiture from 1996) transfered the copyright to all \ 
sources to Gerard Holzmann, explicitly to enable a standard open source release \ 
under the BSD 3-Clause license. Starting with Spin Version 6.4.5 all Spin code, \ 
sources and executables, are now available under the BSD 3-Clause license.
   2017-12-10 14:56:34 by Adam Ciarcinski | Files touched by this commit (3) | Package updated
Log message:
spin: updated to 6.4.7

Version 6.4.7:
- fixed a bug in the parsing of for (...) statements if
  initialized variable declarations appear in the body of the loop
- optimization in interpreting the swarm option, by avoiding
  unnecessary recompilations, plus other small fixes in the
  generation of parameter values for -k and -w with swarms
- added runtime option -W to suppress recompilation of pan if
  the executable already exists
- fixed bug in printing the value of a random seed at the end of
  a randomized run
- added compilation warning if both -DNP and -DNOCLAIM are used
  (in that case -DNP is assumed to override -DNOCLAIM)
- fixed a bug in the parsing of select (...) statements that could
  cause unwarranted syntax errors when larger ranges are used
- switched to executables for Windows PCs that do not require
  a cygwin installation (using mingw32 and mingw64 bit compilations)
   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