47 citations · 134 across the 31 of their papers we have counts for
10 papers · 1 filter
On the Verification Problem of Remote Direct Memory Access programs (Extended Version with Appendix)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Govind Rajanbabu +1
Remote Direct Memory Access (RDMA) is a technology that allows direct memory access from the memory of one computer into that of another without involving either one's operating sy…
Universal Safety for Timed Petri Nets is PSPACE-complete
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu +2
A timed network consists of an arbitrary number of initially identical 1-clock timed automata, interacting via hand-shake communication. In this setting there is no unique central…
Mending Fences with Self-Invalidation and Self-Downgrade
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Stefanos Kaxiras +3
Cache coherence protocols based on self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low e…
Stateless Model Checking for POWER
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson +1
We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines sever…
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…
Proceedings 14th International Workshop on Verification of Infinite-State Systems
Mohamed Faouzi Atig, Ahmed Rezine
This volume contains the proceedings of Infinity'12, the 14th International Workshop on Verification of Infinite-State Systems, which was held in Paris, France on the 27th of Augus…
Adding Time to Pushdown Automata
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jari Stenman
In this tutorial, we illustrate through examples how we can combine two classical models, namely those of pushdown automata (PDA) and timed automata, in order to obtain timed pushd…
Model-Checking of Ordered Multi-Pushdown Automata
Mohamed Faouzi Atig
We address the verification problem of ordered multi-pushdown automata: A multi-stack extension of pushdown automata that comes with a constraint on stack transitions such that a p…
Model checking Branching-Time Properties of Multi-Pushdown Systems is Hard
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar +1
We address the model checking problem for shared memory concurrent programs modeled as multi-pushdown systems. We consider here boolean programs with a finite number of threads and…
Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads
Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer
Context-bounded analysis has been shown to be both efficient and effective at finding bugs in concurrent programs. According to its original definition, context-bounded analysis ex…