Sarbojit Das

dblp:353/2026 · DBLP profile ↗
← Back
2ranked-venue papers
0as first author
2since 2021 · last 2024
0009-0004-7029-1904ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 2 · 2 since 2021Theory of computation · 1 · 1 since 2021
YearPublicationVenuePosition
2024 Parsimonious Optimal Dynamic Partial Order Reduction
abstract
Abstract Stateless model checking is a fully automatic verification technique for concurrent programs that checks for safety violations by exploring all possible thread schedulings. It becomes effective when coupled with Dynamic Partial Order Reduction (DPOR), which introduces an equivalence on schedulings and reduces the amount of needed exploration. DPOR algorithms that are optimal are particularly effective in that they guarantee to explore exactly one execution from each equivalence class. Unfortunately, existing sequence-based optimal algorithms may in the worst case consume memory that is exponential in the size of the analyzed program. In this paper, we present Parsimonious-OPtimal DPOR (POP), an optimal DPOR algorithm for analyzing multi-threaded programs under sequential consistency, whose space consumption is polynomial in the worst case. POP combines several novel algorithmic techniques, including (i) a parsimonious race reversal strategy, which avoids multiple reversals of the same race, (ii) an eager race reversal strategy to avoid storing initial fragments of to-be-explored executions, and (iii) a space-efficient scheme for preventing redundant exploration, which replaces the use of sleep sets. Our implementation in Nidhugg shows that these techniques can significantly speed up the analysis of concurrent programs, and do so with low memory consumption. Comparison to TruSt, a related optimal DPOR algorithm that represents executions as graphs, shows that POP ’s implementation achieves similar performance for smaller benchmarks, and scales much better than TruSt ’s on programs with long executions.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson 0001, Konstantinos Sagonas
CAV (2)3
2023 Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Bønneland, Sarbojit Das, Bengt Jonsson 0001, Magnus Lång, Konstantinos Sagonas
ATVA4