CoLT (Concurrency using Lockstep Tool) is a tool for model checking of linearizability of concurrent data structure implementations.
- Model Checking of Linearizability
of Concurrent List Implementations.
Pavol Cerny, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri and Rajeev Alur
CAV 2010, Edinburgh, UK, July 15th-19th, 2010
- Theoretical background
- Streaming transducers for algorithmic
verification of single-pass list processing
Rajeev Alur and Pavol Cerny
POPL 2011, to appear
- Algorithmic Analysis of Array-Accessing
Rajeev Alur, Pavol Cerny and Scott Weinstein
18th Conference on Computer Science Logic
CSL 2009, Coimbra, Portugal, September 7-11, 2009
- Streaming transducers for algorithmic verification of single-pass list processing programs. New!
Click here to see the examples and results, including visual representation of counterexample traces in cases the tool found not to be linearizable.