Lazy-CSeq: Tool for Sequentializing Concurrent C Programs
Lazy-CSeq is a tool for the sequential analysis of non-deterministic concurrent C programs, offering approaches for reduction to sequential analysis and conversion. It provides solutions for analyzing concurrent programs, unrolling, inlining, and refactoring, as well as testing with various tools like Klee, BMC, and model-checkers. Lazy-CSeq ensures equivalence to various round-robin schedules and offers context bounding capabilities.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Lazy-CSeq A Lazy Sequentialization Tool for C Omar Inverso Ermenegildo Tomasco Bernd Fischer Salvatore La Torre Gennaro Parlato University of Southampton, UK University of Southampton, UK Stellenbosch University, South Africa Universit di Salerno, Italy University of Southampton, UK
CSeq framework problem: analysis of concurrent programs sequential non-deterministic C program concurrent C program sequential analysis tool CSeq P P' approach: reduction to sequential analysis convert concurrent program P into sequential program P' analyse P' using a sequential tool
CSeq framework problem: analysis of concurrent programs unrolling inlining refactoring sequential non-deterministic C program concurrent C program sequential analysis tool CSeq P P' sequentialisation s Lal-Reps Memory-Unwinding Lazy-CSeq approach: reduction to sequential analysis convert concurrent program P into sequential program P' analyse P' using a sequential tool
CSeq framework problem: analysis of concurrent programs sequential non-deterministic C program testing Klee concurrent C program bounded model-checkers BLITZ CBMC ESBMC LLBMC sequential analysis tool CSeq P P' abstraction CPAchecker SATABS approach: reduction to sequential analysis convert concurrent program P into sequential program P' analyse P' using a sequential tool
Lazy-CSeq P' equivalent to P up to k round-robin schedules round bound k sequential non-deterministic C program concurrent C program BMC tool Lazy-CSeq P P'
Lazy-CSeq P' equivalent to P up to k round-robin schedules round bound k sequential non-deterministic C program program unfolding concurrent C program BMC tool Lazy-CSeq P P' context bounding [CAV 14]
Lazy-CSeq P' equivalent to P up to k round-robin schedules round bound k sequential non-deterministic C program program unfolding concurrent C program BMC tool Lazy-CSeq CBMC P P' context bounding [CAV 14]
Lazy-CSeq P' equivalent to P up to k round-robin schedules round bound k sequential non-deterministic C program program unfolding concurrent C program BMC tool Lazy-CSeq CBMC P P' context bounding [CAV 14] improvements on SV-COMP 14 version optimised sequentialisation (less non-determinism, vars, clauses) improved backend support (CPROVER_bitvector, )
Competition Analyse each test case up to 5 times (with increasing bounds) ERROR found UNSAFE no ERROR found increase bounds, restart analysis no ERROR found, last phase SAFE
Competition Analyse each test case up to 5 times (with increasing bounds) ERROR found UNSAFE no ERROR found increase bounds, restart analysis no ERROR found, last phase SAFE Performance no missed bugs no false positives low verification time low memory consumption
Thank You users.ecs.soton.ac.uk/gp4/cseq
