PhD Artifact (SMR verification)

Artifact accompanying PhD thesis: reduction technique from Section 7 (verification of SMR implementations). For more details visit: https://wolff09.github.io/phd/

PhD Artifact (ownership, part2)

Artifact accompanying PhD thesis: ownership technique from Section 6 (tracking version counters for next pointers). For more details visit: https://wolff09.github.io/phd/

PhD Artifact (ownership, part1)

Artifact accompanying PhD thesis: ownership technique from Section 6 (without tracking version counters for next pointers). For more details visit: https://wolff09.github.io/phd/

PhD Artifact (DS verification)

Artifact accompanying PhD thesis: reduction technique from Section 7 (verification of data structure implementations). For more details visit: https://wolff09.github.io/phd/

POPL 2019 Artifact (SMR Implementation Verification)

Artifact accompanying the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019) paper Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis by Roland Meyer and Sebastian Wolff. This release implements the verification of SMR implementations against their specification.

For more details visit: https://wolff09.github.io/TMRexp/

POPL 2019 Artifact (Data Structure Verification)

Artifact accompanying the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019) paper Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis by Roland Meyer and Sebastian Wolff. This release implements the verification of lock-free data structures relative to an SMR specification.

For more details visit: https://www.tcs.cs.tu-bs.de/popl19

POPL 2019 (Artifact Evaluation)

Artifact accompanying the 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019) paper Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis by Roland Meyer and Sebastian Wolff. This release implements the verification of lock-free data structures against an SMR specification. It was submitted to artifact evaluation.

For more details visit: https://wolff09.github.io/TMRexp/

SAS17

Artifact submitted to the 24th Static Analysis Symposium (SAS'17) alongside the paper Effect Summaries for Thread-Modular Analysis by Lukáš Holík, Roland Meyer, Tomáš Vojnar and Sebastian Wolff.

SAS17-GC

Artifact submitted to the 24th Static Analysis Symposium (SAS'17) alongside the paper Effect Summaries for Thread-Modular Analysis by Lukáš Holík, Roland Meyer, Tomáš Vojnar and Sebastian Wolff.

Note that this release is a branch of the tool optimized for an analysis relying on garbage collection. For the main version, capable of handling explicit memory management, see release SAS17