kirancodes.me
To Proof Maintenance & Beyond!
ASE 2013

CSeq: A concurrency pre-processor for sequential C verification tools

Bernd Fischer, Omar Inverso, Gennaro Parlato

DOI 10.1109/ase.2013.6693139dblp

Abstract

Sequentialization translates concurrent programs into equivalent nondeterministic sequential programs so that the different concurrent schedules no longer need to be handled explicitly. It can thus be used as a concurrency preprocessing technique for automated sequential program verification tools. Our CSeq tool implements a novel sequentialization for C programs using pthreads, which extends the Lal/Reps sequentialization to support dynamic thread creation. CSeq now works with three different backend tools, CBMC, ESBMC, and LLBMC, and is competitive with state-of-the-art verification tools for concurrent programs.

BibTeX
@inproceedings{Fischer-al:ASE13,
  author    = {Bernd Fischer and
               Omar Inverso and
               Gennaro Parlato},
  title     = {{CSeq:} A concurrency pre-processor for sequential C verification tools},
  booktitle = {ASE},
  pages     = {710--713},
  publisher = {{IEEE}},
  year      = {2013},
}

Related papers