sliver v4.0

Changes since v3.0

• C translation: general improvements

• LAbS: Added conditional processes (cond => P) (C encoding only)

• LAbS: Added multi-dimensional arrays (e.g., arr[x, y, z]) (C encoding only)

• SLiVER: Fixed ESBMC backend for SMT-based BMC

• SLiVER: Improved performance of CBMC simulation workflow

Additional instructions

After unpacking the zip archive, follow the instructions in README.txt.

sliver v3.0

Changes since v3.0-PREVIEW

• LAbS: Added blocks of actions {a1; a2; ... ; an}

• LAbS: Added block-local variables var := expr

• LAbS: Added a new rounding integer division operator e1 : e2

• LAbS: Added lookup operator var of expr

• LAbS: Added assignment to evaluation of quantified predicates (e.g, b := forall ... or b := exists ...)

• LAbS: Added nondeterministic agent selection pick

• LAbS: Added ternary operator if cond then expr1 else expr2

• LAbS: Underscores (_) can now be used within all names (but not at the beginning of a name)

• LAbS: Arithmetic expressions can now be used where a Boolean expression is expected (expr is desugared into expr != 0)

• SLiVER: CBMC backend now supports simulation

• SLiVER: Added a compositional CADP backend cadp-comp (experimental)

Additional instructions

After unpacking the zip archive, cd to the SLiVER root directory and run the following command:

pip install -r requirements.txt

This will install Z3 and its Python API, needed by the CBMC-based simulation workflow.

sliver v3.0-PREVIEW

• C translation: Support new LAbS features (experimental)
• SLiVER: Added simulation support to CBMC backend (requires Z3)

Caveat

This is a pre-release. The syntax supported here may be subject to chenge.

Additional instructions

After unpacking the zip archive, cd to the SLiVER root directory and run the following command:

pip install -r requirements.txt

This will install Z3 and its Python API, needed by the CBMC-based simulation workflow.

sliver 2.1

Please refer to README.txt for installation and usage instructions.

Changes since v2.0

• C translation: Fixed a bug with the nondeterministic value operator
• C translation: Fixed a bug with counterexample translation
• LAbS: Added an optional "assume { ... }" section to constrain initial states (LAbS-to-C only)
• SLiVER: Fixed a bug in CSeq backend
• SLiVER: Fixed a bug with the --no-properties option
• SLiVER: New CLI option --include

sliver 2.0

Please refer to README.txt for installation and usage instructions.
Note that, from now on, SLiVER requires Python >= 3.8.

Changes since v1.7

• LNT translation: the "cadp" backend uses a new property translation workflow. The old workflow is still available as "cadp-monitor"
• Parser: Fixed a bug with arrays in link predicates and properties
• Parser: Basic support for a new "raw function call" process $call(...)
• SLiVER: Updated dependencies (pyparsing and click)
• SLiVER: Better reporting, especially with --verbose
• SLiVER: New CLI options --property and --no-properties for property selection
• SLiVER: New CLI options --keep-files
• SLiVER: Fixed a bug in CSeq backend's parallel analysis which occasionally led to deadlocks

sliver 1.7

Please refer to README.txt for installation and usage instructions.

Changes since v1.6

• Parser: A new "nondeterministic value" operator [n .. m] is supported (LAbS-to-C only)
• Parser: link predicates now support "of 1", "of 2" in addition to the legacy syntax "of c1", "of c2"
• LNT translation: code generator now follows the new LNT syntax (CADP 2021-d)
• LNT translation: more efficient encoding of timestamps

sliver 1.6

Please refer to README.txt for installation and usage instructions.

Changes since v1.5

• LNT translation: code generator now follows the new LNT syntax
• LNT translation: fix a CADP verification query

sliver 1.5

Please refer to README.txt for installation and usage instructions.

Changes since v1.4

• LabsTranslate: improve simplification of Boolean expressions
• LNT translation: general improvements
• LNT translation: adapted to new LNT syntax (CADP 2020-d and beyond)
• C translation: disable stigmergies and/or environment when not needed
• C translation: remove all preprocessor directives
• SLiVER: CBMC backend now compatible with cbmc > 5.10
• SLiVER: Improved cleanup of intermediate files
• SLiVER: Support CSeq-1.9

sliver 1.4

Please refer to README.txt for installation and usage instructions.

Please note that sliver-v1.3 was an internal release.

Changes since v1.2

Version 1.4 - 2020-02

• LNT translation: disable stigmergies and/or environment when not needed
• SLiVER: fixed several bugs related to CADP backend
• SLiVER: added counterexample translations for CADP backend

Version 1.3 - 2019-11 (internal release)

• LabsTranslate: General improvements to parser/code generator
• LabsTranslate: Fixed a bug when using external variables in array subscript
• LabsTranslate: Added LNT translation (experimental)
• LabsTranslate: Remove (some) redundant sub-predicates from "finally"/"always" assertions
• SLiVER: Added support to generate unbounded encodings
• SLiVER: Updated bundled CSeq backend, improved support for parallel analysis
• C translation: Disable stigmergy encoding when not needed
• C translation: General improvements

sliver v1.2

Please refer to README.txt for installation and usage instructions.