-
Notifications
You must be signed in to change notification settings - Fork 0
/
HISTORY
101 lines (79 loc) · 4.3 KB
/
HISTORY
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
Version 5.1 - 2024-11
SLiVER: Fixed a bug with CBMC counterexample parsing
LAbS: Updated/improved bundled examples
Version 5.0 - 2024-11
C translation: general improvements
LAbS: Added counting assignment to local variable (e.g., "c := count Agent x, ...")
LAbS: Improved syntax of link expressions (used for stigmergies and pick instructions)
Version 4.0 - 2023-05
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
Version 3.0 - 2022-07
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)
Version 2.1 - 2021-11
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`
Version 2.0 - 2021-10
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 option `--keep-files`
SLiVER: Fixed a bug in CSeq backend's parallel analysis which occasionally led to deadlocks
Version 1.7 - 2021-07
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
Version 1.6 - 2021-01
LNT translation: Code generator now follows the new LNT syntax (CADP 2021-a)
LNT translation: Fix a CADP verification query
Version 1.5 - 2020-10
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
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
Version 1.2 - 2019-06
LabsTranslate: Improved intermediate representation
Version 1.1 - 2018-11 (internal release)
LabsTranslate: Improved/updated parser
C translation: General improvements
C translation: Support for generating __CPROVER_bitvector[] typedefs
Version 1.0 - 2018-05
Initial release of SLiVER