Cited in
(36)- Horn clauses as an intermediate representation for program analysis and transformation
- Predicate abstraction for program verification
- Lost in abstraction: monotonicity in multi-threaded programs
- Practical abstractions for automated verification of shared-memory concurrency
- Analysis of correct synchronization of operating system components
- Cseq
- CPAchecker
- Predator
- UFO
- ACL2s
- SymmExtractor
- SymmPa
- HSF
- SLAB
- Orion
- Lazy-CSeq
- MAGIC
- LCTD
- Regression verification for multi-threaded programs
- monabs
- LOCKSMITH
- RELAY
- Ultimate Kojak
- CPAlien
- FrankenBit
- Jakstab
- MU-CSeq
- Symbiotic 2
- LCT
- CIVL
- Regression verification for multi-threaded programs (with extensions to locks and dynamic thread creation)
- Precise thread-modular abstract interpretation of concurrent programs using relational interference abstractions
- Combining model checking and data-flow analysis
- Software verification for weak memory via program transformation
- LCTD: test-guided proofs for C programs on LLVM
- Counterexample-guided abstraction refinement for symmetric concurrent programs
This page was built for software: Threader
