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.
- Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Model
- BMC with Memory Models as Modules
- BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings
- Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)
- Dartagnan: Leveraging Compiler Optimizations and the Price of Precision (Competition Contribution)
- Dartagnan: SMT-based Violation Witness Validation (Competition Contribution)