logo


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, where the non-determinism allows to handle different concurrent schedules collectively.
This approach has three main advantages:

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:

Lazy-CSeq

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.

MU-CSeq

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.

UL-CSeq

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.

Lal-Reps CSeq    

Lal-Reps 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 to support dynamic thread creation.

Publications

  1. MU-CSeq 0.4: IndividualMemory 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)

  2. 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)

  3. 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)

  4. Bounded Model Checking of Multi-threaded Programs via Sequentialization
    O. Inverso.
    PhD Thesis, University of Southampton,  2015.
    (PDF)

  5. 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)

  6. 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)

  7. 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)

  8. 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)

  9. 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)

  10. 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)

  11. 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)

  12. 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)

  13. 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)

  14. 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)

People

CSeq is developed by :