Tools

I'm the maintainer of Dartagnan, a tool to analyse concurrent programs running on weak memory models such x86-TSO, ARMv8, Power, RISCV or the Linux kernel memory model (LKMM).

Since 2020, Dartagnan participates in SVCOMP.

Related publications:

  1. Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Model
  2. BMC with Memory Models as Modules
  3. BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
  4. Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)
  5. Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution)
  6. Dartagnan: SMT-based Violation Witness Validation (Competition Contribution)
  7. CAAT: Consistency as a Theory

social