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:

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

VeriSmart

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

• Publications:
• ASE'17
  


• Downloads:
• VeriSmart-1.0 (2017.09.11), experiments

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.

• Publications:
• FMCAD'16
  
• ASE'15
  
• CAV'14
• SV-COMP'14
  
  
• Downloads:
• 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'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

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:
• SV-COMP'16
• TACAS'15
• SV-COMP'15
  
• SV-COMP'14
  
  
• 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

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:
• ATVA'16
  
• SV-COMP'16
  
• SV-COMP'15
  
  
• Downloads:
• UL-CSeq-0.2 (ATVA'16 version)
  
• UL-CSeq-0.1 (SV-COMP'15 version)
  
  
• Supported backends:
• CBMC
• CPAChecker
  
• SeaHorn
• Ultimate Automizer
  
• VVT
  
  
• SV-COMP results:
• 2016
• 2015

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:
• ASE'13
• SV-COMP'13
  
  
• 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
  
  
• SV-COMP results:
• 2013

Publications

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


2. 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)
   
   
3. 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)
   
   
4. 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)
   
   
5. 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)
   
   
6. Bounded Model Checking of Multi-threaded Programs via Sequentialization
   O. Inverso.
   PhD Thesis, University of Southampton,  2015.
   (PDF)
   
   
7. 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)
   
   
8. 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)
   
   
9. 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)
   
   
10. 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)
    
    
11. 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)
    
    
12. 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)
    
    
13. 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)
    
    
14. 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)
    
    
15. 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)
    
    
16. 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

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

Funding

Download Form

Please fill the form below. The download link will be sent to your mail automatically.

Security test, please identify the pictures.
identify... Apple Cat Clock Dog Flower Fork Hammer Key Ship Tree	identify... Apple Cat Clock Dog Flower Fork Hammer Key Ship Tree	identify... Apple Cat Clock Dog Flower Fork Hammer Key Ship Tree

Download