v2.5.0

This release adds a --version option to the command line tools.

v2.4.2

This release fixes some warnings and style issues in the XSTS (and related) projects.

v2.4.1

This release fixes a bug when comparing top/bottom states.

v2.4.0

This release adds algorithmic support to bitvectors in the theta-cfa-cli tool via new refinement strategies. Previous strategies (e.g., SEQ_ITP) did not work for bitvectors because the underlying Z3 solver does not support interpolation over bitvectors. The new strategies are based on unsat core predicates and the Newton approach. Note that these algorithms are still in an experimental phase, we are working on their benchmarking and fine-tuning. Credits go to @as3810t.

v2.3.0

This release introduces a breaking change in the syntax (and semantics) of bitvectors. Previously, bitvector variables could be declared with signedness information (signed/unsigned) and the operations relied on this information. With this release, bitvector variables no longer store their signedness (i.e., there is a single bitvector type with only the length as a parameter). Operations where signedness matters (e.g., comparison) come in two flavors (e.g., sgt for signed greater-than and ugt for unsigned greater-than). This aligns with the way SMT-LIB and LLVM works. Thanks @as3810t! See bitvectors.md for more information.

v2.2.1

This patch adds integration tests to CFA and STS analysis projects and some improvements for error reporting in parsers.

v2.2.0

This release introduces a slight change in error reporting of the CLI tools. Errors are now more localized (parsing/algorithm/etc.).

v2.1.0

This release improves error reporting. The message of the exception is printed by default and a new --stacktrace option is added to CLI tools to print the full stack trace regardless of the logging level.

v2.0.1

This release fixes some warnings and changes the default value of the --maxenum flag of cfa-cli to 10 (instead of 0), which usually gives a better performance.

v2.0.0

This major release adds a new formalism, the eXtended Symbolic Transition System (XSTS), including a textual DSL, analysis modules and a command-line tool running CEGAR-based analyses. The XSTS formalism is a backend to the Gamma Statechart Composition Framework, where it can analyze reachability queries over collaborating state machines. Note that the XSTS formalism and related projects are still experimental, major changes and improvements are expected. Big thanks to @mondokm @grbeni @vincemolnar