7 citations · 8 across the 6 of their papers we have counts for
6 papers
Verification under TSO with an infinite Data Domain
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach +1
We examine verification of concurrent programs under the total store ordering (TSO) semantics used by the x86 architecture. In our model, threads manipulate variables over infinite…
Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Meyer Bønneland +4
Event-driven multi-threaded programming is an important idiom for structuring concurrent computations. Stateless Model Checking (SMC) is an effective verification technique for mul…
Optimal Reads-From Consistency Checking for C11-Style Memory Models
Hünkar Can Tunç, Parosh Aziz Abdulla, Soham Chakraborty +3
Over the years, several memory models have been proposed to capture the subtle concurrency semantics of C/C++.One of the most fundamental problems associated with a memory model M…
Parameterized Verification under TSO with Data Types
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach +4
We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially inf…
Stateless Model Checking for TSO and PSO
Parosh Abdulla, Stavros Aronis, Mohammed Faouzi Atig +3
We present a technique for efficient stateless model checking of programs that execute under the relaxed memory models TSO and PSO. The basis for our technique is a novel represent…
Infinite-State Energy Games
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman +3
Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensiona…