Seminars

View all Seminars  |  Download ICal for this event

ViEqui: Optimal Stateless Model Checking based on View Equivalence

Series: Department Seminar

Speaker: Subodh Sharma

Date/Time: Jan 31 11:00:00

Location: CSA Auditorium, (Room No. 104, Ground Floor)

Abstract:
Partitioning program executions into equivalence classes is a cornerstone of efficient stateless model checking for concurrent programs. This talk introduces view-equivalence, a novel partitioning relation based on the values read by memory accesses. Two executions are considered view-equivalent if they share the same set of read memory accesses and these accesses read identical values. View-equivalence minimizes the number of equivalence classes compared to existing relations, offering a coarser partitioning while preserving correctness and completeness. The talk also presents ViEqui, a stateless model checker built on this relation, implemented for C/C++ programs using the Nidhugg tool. Extensive testing on over 16,000 litmus tests demonstrates ViEqui\'s soundness and optimality, achieving over 50x speedup in ~20% of tests and outperforming existing techniques by timing out in significantly fewer cases on challenging benchmarks.

Speaker Bio:
Subodh Sharma is a Associate Professor and Pankaj Gupta Chair Professor in the Computer Science and Engineering Department at IIT Delhi. He works primarily in the area of software engineering and formal methods, with a focus on ensuring reliability of parallel software using static and dynamic program analyses, model checking, and PL techniques.

Host Faculty: Deepak D'Souza