Skip to content

sliver v3.0
Compare
Choose a tag to compare
@lou1306 lou1306 released this 19 Jan 20:48
· 152 commits to master since this release
v3.0
18a49fc
This commit was signed with the committer’s verified signature.
lou1306 Luca Di Stefano
GPG key ID: 826AB2A4C8A549F2
Learn about vigilant mode.

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.

Assets 3
Loading