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.

LaDR (github) is a symbolic static data race detection tool that modifies Lazy-CSeq's code-to-code translation to inject additional code that monitors all accesses to shared memory locations.

Publications:

• Static Data Race Detection via Lazy Sequentialization. B. Fischer, G. Garbi S. La Torre, G. Parlato, and P. Schrammel. 12th International Conference on Networked Systems NETYS 2024, Rabat, Morocco, May 29-31, 2024, pp. 124-141, LNCS 14783.

Downloads:

• LaDR 0.1 (Netys version, 2024.08.20)

VeriSmart is a novel parallel bug-finding framework for concurrent C programs built on top of Lazy-CSeq. It uses a parametrizable code-to-code translation to generate a set of simpler program instances, each capturing a reduced set of the original program's interleavings. These instances are then checked independently in parallel. With a small number of cores it found bugs in the hardest known concurrency benchmarks in a matter of minutes, whereas other dynamic and static tools fail to do so in hours.

Publications:

• VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-threaded Programs with Lazy-CSeq. B. Fischer, S. La Torre, and G. Parlato. 34th IEEE/ACM International Conference on Automated Software Engineering, (ASE), San Diego, CA, USA, 2019, pp. 1150-1153.
• Parallel bug-finding in concurrent programs via reduced interleaving instances. T. L. Nguyen, Peter Schrammel B. Fischer, S. La Torre, and G. Parlato. 32nd IEEE/ACM International Conference on Automated Software Engineering, (ASE), Urbana, IL, USA, 2017, pp. 753-764. (preprint)

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. (preprint)
• 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. (preprint)
• 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. (preprint)
• 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. (preprint)
  
• 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. (preprint)
• 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, (preprint)

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:

• Silver medal in concurrency category at SV-COMP'22
• Gold medal in concurrency category at SV-COMP'21
• Gold medal in concurrency category at SV-COMP'20
• Silver medal in concurrency category at SV-COMP'19
• 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:

• 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. (preprint)
• 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. (preprint)
  
• 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. (preprint)
• 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. (preprint)

Downloads:

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

Awards:

• 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:

• 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. (preprint)
• 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. (preprint)
• 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. (preprint)

Downloads:

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

Supported backends:

• CBMC
• CPAChecker
• SeaHorn
• Ultimate Automizer
• VVT

LR-CSeq (originally simply called 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, pp. 710-713. (preprint)
• 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, pp. 616-618, LNCS 9035. (preprint)

Downloads:

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

Awards:

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

Supported backends:

• CBMC
• ESBMC
• LLBMC

• 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:

• Bernd Fischer (University of Stellenbosch, South Africa)
• Giulio Garbi (University of Molise, Pesche, Italy)
• Omar Inverso (Gran Sasso Science Institute (GSSI), L'Aquila, Italy)
• Salvatore La Torre (University of Salerno, Fisciano, Italy)
• Truc L. Nguyen (University of Southampton, UK)
• Gennaro Parlato (project leader, University of Molise, Pesche, Italy)
• Peter Schrammel (Diffblue Ltd, Oxford, UK)
• Ermenegildo Tomasco (University of Southampton, UK)

This work was partially supported by INDAM-GNCS 2019-2025 and 2021 Visiting Professor grants, by EPSRC grants EP/M008991/1 and EP/P022413/1, by the University of Southampton Scholarship Schemes, by the AWS 2021 Amazon Research Awards, by the MUR projects "Future Artificial Intelligence Research" (FAIR) and "Innovation, digitalization and sustainability for the diffused economy in Central Italy", Spoke 1 MEGHALITIC, VITALITY Ecosystem, by the PRIN projects DREAM (20228FT78M) and PNRR DeLICE (F53D23009130001), by MUR-PNRR VITALITY (ECS00000041), by the MUR projects SOP (Securing sOftware Platforms, CUP: H73C22000890001) as part of the SERICS project (n. PE00000014 - CUP: B43C22000750006), by FARB 2020-2022 grants from Università degli Studi di Salerno, and by the ERASMUS+ International Credit Mobility Project 2024-1-IT02-KA171-HED-000224869.