kirancodes.me
To Proof Maintenance & Beyond!
ASE 2015

Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-threaded C-Programs

Omar Inverso, Truc L. Nguyen, Bernd Fischer, Salvatore La Torre, Gennaro Parlato

DOI 10.1109/ase.2015.108dblp

Abstract

Lazy-CSeq is a context-bounded verification tool for sequentially consistent C programs using POSIX threads. It first translates a multi-threaded C program into a bounded nondeterministic sequential C program that preserves bounded reachability for all round-robin schedules up to a given number of rounds. It then reuses existing high-performance bounded model checkers as sequential verification backends. Lazy-CSeq handles the full C language and the main parts of the POSIX thread API, such as dynamic thread creation and deletion, and synchronization via thread join, locks, and condition variables. It supports assertion checking and deadlock detection, and returns counterexamples in case of errors. Lazy-CSeq outperforms other concurrency verification tools and has won the concurrency category of the last two SV-COMP verification competitions.

BibTeX
@inproceedings{Inverso-al:ASE15,
  author    = {Omar Inverso and
               Truc L. Nguyen and
               Bernd Fischer and
               Salvatore La Torre and
               Gennaro Parlato},
  title     = {{Lazy-CSeq:} A {Context-Bounded} Model Checking Tool for Multi-threaded {C-Programs}},
  booktitle = {ASE},
  pages     = {807--812},
  publisher = {{IEEE} Computer Society},
  year      = {2015},
}

Related papers