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
        [pdf] [bib]
  • Theoretical background
    • Streaming transducers for algorithmic verification of single-pass list processing programs. New!
          Rajeev Alur and Pavol Cerny
          POPL 2011, to appear
    • Algorithmic Analysis of Array-Accessing Programs.
          Rajeev Alur, Pavol Cerny and Scott Weinstein
          18th Conference on Computer Science Logic
          CSL 2009, Coimbra, Portugal, September 7-11, 2009

          [pdf] [bib]


We evaluated the tool on a representative sample of Java implementations of the concurrent set data structure. The tool verified linearizability of a number of implementations, found a known error in a lock-free implementation and proved that the corrected version is linearizable.

Click here to see the examples and results, including visual representation of counterexample traces in cases the tool found not to be linearizable.


Rajeev Alur, UPenn
Pavol Cerny, IST Austria
Swarat Chaudhuri, Penn State
Arjun Radhakrishna, IST Austria
Damien Zufferey, IST Austria