Name
Abstract | ||
|---|---|---|
This paper reports progress in verification tool engineering for weak memory models. We present two bounded model checking tools for concurrent programs. Their distinguishing feature is modularity: Besides a program, they expect as input a module describing the hardware architecture for which the program should be verified. DARTAGNAN verifies state reachability under the given memory model using a novel SMT encoding. PORTHOS checks state equivalence under two given memory models using a guided search strategy. We have performed experiments to compare our tools against other memory model-aware verifiers and find them very competitive, despite the modularity offered by our approach. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.23919/FMCAD.2018.8603021 | 2018 Formal Methods in Computer Aided Design (FMCAD) |
Keywords | Field | DocType |
Memory models,CAT,concurrent programs,bounded model checking,SMT encodings | Model checking,Computer science,Instruction set,Theoretical computer science,Reachability,Memory model,Concurrent computing,Modularity,Hardware architecture,Encoding (memory) | Conference |
ISBN | Citations | PageRank |
978-1-5386-7567-0 | 0 | 0.34 |
References | Authors | |
25 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hernán Ponce de León | 1 | 7 | 2.16 |
| Florian Furbach | 2 | 4 | 1.75 |
| Keijo Heljanko | 3 | 751 | 47.90 |
| Roland Meyer | 4 | 13 | 8.39 |