Name
Abstract | ||
|---|---|---|
Previous work formalized the C++ memory model in Isabelle/HOL in an effort to clarify the proposed standard's semantics. Here we employ the model finder Nitpick to check litmus test programs that exercise the memory model, including a simple locking algorithm. Nitpick is built on Kodkod (Alloy's backend) but understands Isabelle's richer logic; hence it can be applied directly to the C++ memory model. We only need to give it a few hints, and thanks to the underlying SAT solver it scales much better than the Cppmem explicit-state model checker. This case study inspired optimizations in Nitpick from which other formalizations can now benefit. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1145/2003476.2003493 | PPDP |
Keywords | Field | DocType |
proposed standard,model finder nitpick,underlying sat solver,memory model,cppmem explicit-state model checker,previous work,richer logic,case study,litmus test program,computer programming,sat solver,higher order logic,concurrency | HOL,Model checking,Programming language,Computer science,Concurrency,Boolean satisfiability problem,Theoretical computer science,Memory model,Semantics,Computer programming,Higher-order logic | Conference |
Citations | PageRank | References |
12 | 0.70 | 18 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jasmin Christian Blanchette | 1 | 530 | 39.61 |
| Tjark Weber | 2 | 215 | 19.33 |
| Mark Batty | 3 | 203 | 9.21 |
| Scott Owens | 4 | 683 | 26.50 |
| Susmit Sarkar | 5 | 744 | 30.76 |