Sequentialization is a technique for the analysis of concurrent programs that exploits verification techniques or tools that were originally designed for sequential programs. Sequentialization can be implemented as a code-to-code translation from the concurrent program into a corresponding non-deterministic sequential program that simulates all executions of the original program. The sequential program contains both the mapping of the threads in the form of functions, and an encoding of the scheduler, were the non-determinism allows to handle different concurrent schedules collectively. This approach has three main advantages:

• a code-to-code translation is typically much easier to implement than a full-fledged analysis tool;
• it allows designers to focus only on the concurrency aspects of programs, delegating all sequential reasoning to an existing target analysis tool;
• sequentializations can be designed to target multiple backends for sequential program analysis.

CSeq is a framework that facilitates the development of code-to-code translations for concurrent C programs with POSIX threads based on sequentialization. The following are verification tools that have been developed under the CSeq framework.

VeriSmart is a novel parallel bug-finding framework for concurrent C programs.

Publications:

• (full reference missing) ASE'17

Downloads:

• VeriSmart-1.0(2017.09.11), experiments

Lazy-CSeq is a code-to-code transformation tool that translates a multi-threaded C program into a nondeterministic sequential C program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. It re-uses existing high-performance BMC tools as backends for the sequential verification problem. The translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so that it produces tight SAT/SMT formulae, and is thus very effective in practice. The tool has a script that bundles the translation and the verification.

Publications:

• Lazy Sequentialization for TSO and PSO via Shared Memory Abstractions. E. Tomasco, T. L. Nguyen, O. Inverso, B. Fischer, S. La Torre, and G. Parlato. Formal Methods in Computer-Aided Design (FMCAD) Mountain View, CA, USA, 2016. (PDF)
• Lazy-CSeq 1.0 (Competition Contribution). O. Inverso, T. L. Nguyen, E. Tomasco, B. Fischer, S. La Torre, and G. Parlato. 5th Intl. Competition on Software Verification (SV-COMP), held at TACAS, Eindhoven, The Netherlands 2016. (PDF)
• Lazy-CSeq: A Context-Bounded Model Checking Tool for Multi-Threaded C-Programs (Tool Demonstration). O. Inverso, T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato. 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), Lincoln, Nebraska, USA, 2015. (PDF)
• Lazy-CSeq 0.6c: An Improved Lazy Sequentialization Tool for C (Competition Contribution). O. Inverso, E. Tomasco, B. Fischer, S. La Torre, and G. Parlato. 4th Intl. Competition on Software Verification (SV-COMP), held at TACAS, London, UK, 2015. (PDF)
  
• Bounded Model Checking of Multi-Threaded C Programs via Lazy Sequentialization. O. Inverso, E. Tomasco, B. Fischer, S. La Torre, and G. Parlato. 26th Int'l Conference on Computer Aided Verification (CAV), Vienna, Austria, 2014. (PDF)
• Lazy-CSeq: A Lazy Sequentialization Tool for C (Competition Contribution). O. Inverso, E. Tomasco, B. Fischer, S. La Torre, and G. Parlato. 3rd Intl. Competition on Software Verification (SV-COMP), held at TACAS, Grenoble, France, 2014, (PDF)

Downloads:

• Lazy-CSeq-3.0 (TOPLAS version, 2021.05.12)
• Lazy-CSeq-2.0 (2017.02.14)
• Lazy-CSeq-1.0 (2016.01.31), experiments and demo video
• Lazy-CSeq-0.6c (SVCOMP'15 version)

Awards: (incomplete)

• Silver medal in concurrency category at SV-COMP'16
• Gold medal in concurrency category at SV-COMP'15
• Gold medal in concurrency category at SV-COMP'14

Supported backends: (incomplete)

• CBMC
• ESBMC
• LLBMC

MU-CSeq is a code-to-code translation tool for the verification of multi-threaded C programs with POSIX threads. It is based on sequentializing the programs according to a guessed sequence of write operations in the shared memory (memory unwinding, MU). The original algorithm (implemented in MU-CSeq 0.1) stores the values of all shared variables for each write (read-explicit fine-grained MU), which requires multiple copies of the shared variables. Our new algorithms (in MU-CSeq 0.3) store only the writes (read-implicit MU) or only a subset of the writes (coarse-grained MU), which reduces the memory footprint of the unwinding and so allows larger unwinding bounds.

Publications:

• MU-CSeq 0.4: Individual Memory Location Unwindings (Competition Contribution). E. Tomasco, T. L. Nguyen, O. Inverso, B. Fischer, S. La Torre, and G. Parlato. 5th Intl. Competition on Software Verification (SV-COMP), held at TACAS, Eindhoven, The Netherlands, 2016. (PDF)
• MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings (Competition Contribution). E. Tomasco, O. Inverso, B. Fischer, S. La Torre, and G. Parlato. 3rd Intl. Competition on Software Verification (SV-COMP), held at TACAS, Grenoble, France, 2014. (PDF)
  
• Verifying Concurrent Programs by Memory Unwinding. E. Tomasco, O. Inverso, B. Fischer, S. La Torre, and G. Parlato. 21st Int'l Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), London, UK, 2015. (PDF)
• MU-CSeq 0.3: Sequentialization by Read-implicit and Coarse-grained Memory Unwindings (Competition Contribution). E. Tomasco, O. Inverso, B. Fischer, S. La Torre, and G. Parlato. 4th Intl. Competition on Software Verification (SV-COMP), held at TACAS,< London, UK, 2015. (PDF)

Downloads:

• MU-CSeq-0.4 (SV-COMP'16 version)
• MU-CSeq-0.3 (SV-COMP'15 version)

Awards: (incomplete)

• Gold medal in concurrency category at SV-COMP'16
• Silver medal in concurrency category at SV-COMP'15
• Silver medal in concurrency category at SV-COMP'14

Supported backends: (incomplete)

• CBMC

UL-CSeq is a code-to-code translation tool for the verification of multi-threaded C programs with dynamic thread creation. This tool implements a variation of the lazy sequentialization algorithm implemented in Lazy-CSeq. The main novelty is that UL-CSeq supports an unbounded number of context switches and allow unbounded loops, while the number of allowed threads still remains bounded.

Publications:

• Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs. T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato. 14th International Symposium on Automated Technology for Verification and Analysis (ATVA) Chiba, Japan, 2016. (PDF)
• Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C with unboundedly many Context Switches (Competition Contribution). T. L. Nguyen, O. Inverso, E. Tomasco, B. Fischer, S. La Torre, and G. Parlato. 5th Intl. Competition on Software Verification (SV-COMP), held at TACAS, Eindhoven, The Netherlands, 2016. (PDF)
• Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches (Competition Contribution). T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato. 4th Intl. Competition on Software Verification (SV-COMP), held at TACAS, London, UK, 2015. (PDF)

Downloads:

• UL-CSeq-0.2 (ATVA'16 version)
• UL-CSeq-0.1 (SV-COMP'15 version)

Supported backends: (incomplete)

• CBMC
• CPAChecker
• SeaHorn
• Ultimate Automizer
• VVT

LR-CSeq is a code-to-code translation tool which implements a novel sequentialization for C programs using POSIX threads, which extends the Lal/Reps sequentialization schema to support dynamic thread creation.

Publications:

• CSeq: A Concurrency Pre-processor for Sequential C Verification Tools (Tool Demonstration). B. Fischer, O. Inverso, and G. Parlato.
  28th IEEE/ACM International Conference on Automated Software Engineering (ASE), Palo Alto, CA, USA, 2013. (PDF)
• CSeq: A Sequentialization Tool for C (Competition Contribution). B. Fischer, O. Inverso, and G. Parlato. 2nd Intl. Competition on Software Verification (SV-COMP), held at TACAS, Rome, Italy, 2013. (PDF)

Downloads:

• CSeq-0.5 (ASE version, includes benchmarks, demo video)
• CSeq-0.1a (SV-COMP'13 version)

Awards:

• Silver medal in concurrency category at SV-COMP'13

Supported backends: (incomplete)

• ...

• A Pragmatic Verification Approach for Concurrent Programs. T. Nguyen Lam. PhD Thesis, University of Southampton, 2017. (PDF)
• Separating computation from communication:: a design approach for concurrent bug finding. E. Tomasco. PhD Thesis, University of Southampton, 2017. (PDF)
• Bounded Model Checking of Multi-threaded Programs via Sequentialization. O. Inverso. PhD Thesis, University of Southampton, 2015. (PDF)

CSeq is developed by:

• Omar Inverso (University of Southampton, UK)
• Truc L. Nguyen (University of Southampton, UK)
• Ermenegildo Tomasco (University of Southampton, UK)
• Bernd Fischer (University of Stellenbosch, South Africa)
• Salvatore La Torre (University of Salerno, Italy)
• Gennaro Parlato (University of Southampton, UK)

This project is partially supported by EPSRC.