Skip to content

Dat3M 3.1.0 is out!
Compare
Choose a tag to compare
@hernanponcedeleon hernanponcedeleon released this 04 Sep 19:45
· 447 commits to master since this release
3.1.0
d693169

These are the main changes of this version:

  • Implements the theory solver for CAAT (Consistency as a Theory) as described in the OOSPLA’22 paper
  • Adds support for checking liveness
  • Adds support to RC11, IMM and RISCV memory models
  • Updates the support to the latests version of LKMM (including data races)
  • Implements the compilation schemes from LKMM to hardware models
  • Adds macro __VERIFIER_loop_bound to use different unrolling bounds for specific loops
  • Adds option encoding.wmm.idl2sat to encode acyclicity constraint using SAT instead of IDL
  • Adds option witness.graphviz to generate violation graphs
  • Updates JavaSMT version to 3.13.3
  • Several bug fixing and performance improvements
Assets 2
Loading