Skip to content

Dat3M 4.0.0 is out!
Compare
Choose a tag to compare
@hernanponcedeleon hernanponcedeleon released this 02 Jan 10:09
· 138 commits to master since this release
4.0.0
024bd43
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Verified
Learn about vigilant mode.

These are the main changes of this version:

  • More precise support of the C language (function pointers, dynamic memory allocation, dynamic thread creation, and recursion)
  • Support llvm files as input
  • Remove boogie as supported input format
  • Remove dependencies on smack and atomic-replace pass
  • Implement static analysis of memory models, as described in the OOSPLA’23 paper
  • Support for PTX (v6.0 and v7.5) and vulkan memory models
  • Several changes related to SVCOMP 2024 participation
  • Support for many intrinsics (pthread, llvm, UBSAN)
  • Update JavaSMT to version 4.1.0
  • Fix unsoundness of symmetry learning
  • Optimize memory consumption for RA sets
  • Bound refining (CAAT)
  • Update LKMM to latest version
  • Support SRCU for LKMM
  • Allow to update relations in cat
  • Improve user output (lines of code and call stack related to violations / witnesses)
  • Add coverage report
  • Make semantics of pthread events closer to reality
  • Force addresses to be even (as in reality)
  • Fix / improve liveness encoding
  • Improve performance of alias analysis
  • Improve / fix compilation schemes
  • Replace constant propagation by sparse conditional constant propagation
  • Improve most program transformation passes
  • Fix refinement cutting
  • Add support for ARM-based MacOS
  • Move to java 17
  • Several refactors / bug fixing
Assets 2
Loading