Checkfence
From MaRDI portal
Cited in
(29)- Model checking concurrent programs
- Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations
- On automation in the verification of software barriers: experience report
- Effective Program Verification for Relaxed Memory Models
- Symbolic predictive analysis for concurrent programs
- Exploiting step semantics for efficient bounded model checking of asynchronous systems
- Sound and complete monitoring of sequential consistency for relaxed memory models
- Model checking transactional memories
- Stateless model checking for TSO and PSO
- POEM
- Verification of Concurrent Programs on Weak Memory Models
- Atomizer
- Velodrome
- Memorax
- SingleTrack
- UMM
- Java Grande
- Lazy-CSeq
- Weak2SC
- Antichains
- CHESS
- Counter-Example Guided Fence Insertion under TSO
- Memory model sensitive bytecode verification
- Deciding Robustness against Total Store Ordering
- Software verification for weak memory via program transformation
- Formalising Java’s Data Race Free Guarantee
- Verification of STM on relaxed memory models
- Software Transactional Memory on Relaxed Memory Models
- A high-level semantics for program execution under total store order memory
This page was built for software: Checkfence
