./devel/spin, Tool for formal verification of multi-threaded software applications

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


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

Filesize: 5942.288 KB

Version history: (Expand)


CVS history: (Expand)


   2023-07-11 13:07:05 by Thomas Klausner | Files touched by this commit (4) | Package updated
Log message:
spin: update to 6.5.2.

No changelog found, couple of years of development.

pkgsrc change: Install examples.
   2021-10-26 12:20:11 by Nia Alarie | Files touched by this commit (3016)
Log message:
archivers: Replace RMD160 checksums with BLAKE2s checksums

All checksums have been double-checked against existing RMD160 and
SHA512 hashes

Could not be committed due to merge conflict:
devel/py-traitlets/distinfo

The following distfiles were unfetchable (note: some may be only fetched
conditionally):

./devel/pvs/distinfo pvs-3.2-solaris.tgz
./devel/eclipse/distinfo eclipse-sourceBuild-srcIncluded-3.0.1.zip
   2021-10-07 15:44:44 by Nia Alarie | Files touched by this commit (3017)
Log message:
devel: Remove SHA1 hashes for distfiles
   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.