Zobrazeno 1 - 10
of 127
pro vyhledávání: '"Atig, Mohamed Faouzi"'
Autor:
Abdulla, Parosh Aziz, Atig, Mohamed Faouzi, Das, Sarbojit, Jonsson, Bengt, Sagonas, Konstantinos
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)
Externí odkaz:
http://arxiv.org/abs/2405.11128
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 domains and they can check whether variables are related for a range
Externí odkaz:
http://arxiv.org/abs/2401.10423
Autor:
Abdulla, Parosh Aziz, Atig, Mohamed Faouzi, Bønneland, Frederik Meyer, Das, Sarbojit, Jonsson, Bengt, Lång, Magnus, Sagonas, Konstantinos
Event-driven multi-threaded programming is an important idiom for structuring concurrent computations. Stateless Model Checking (SMC) is an effective verification technique for multi-threaded programs, especially when coupled with Dynamic Partial Ord
Externí odkaz:
http://arxiv.org/abs/2307.15930
Autor:
Abdulla, Parosh Aziz, Atig, Mohamed Faouzi, Godbole, Adwait, Krishna, Shankaranarayanan, Vahanwala, Mihir
We consider the verification of omega-regular linear temporal properties of concurrent programs running under weak memory semantics. We observe that in particular, these properties may enforce liveness clauses, whose verification in this context is s
Externí odkaz:
http://arxiv.org/abs/2305.17605
Autor:
Abdulla, Parosh Aziz, Atig, Mohamed Faouzi, Furbach, Florian, Godbole, Adwait, Hendi, Yacoub G., Krishna, Shankaranarayanan, Spengler, Stephan
We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability
Externí odkaz:
http://arxiv.org/abs/2302.02163
Autor:
Abdulla, Parosh Aziz, Atig, Mohamed Faouzi, Gupta, Ashutosh, Krishna, Shankaranarayanan, Tuppe, Omkar
We present a framework for efficient stateless model checking (SMC) of concurrent programs under five prominent models of causal consistency, CCv,CM,CC, Read Committed and Read Atomic. Our approach is based on exploring traces under the program order
Externí odkaz:
http://arxiv.org/abs/2211.09020
We present $\textit{Probabilistic Total Store Ordering (PTSO)}$ -- a probabilistic extension of the classical TSO semantics. For a given (finite-state) program, the operational semantics of PTSO induces an infinite-state Markov chain. We resolve the
Externí odkaz:
http://arxiv.org/abs/2201.10213
Autor:
Abdulla, Parosh Aziz, Atig, Mohamed Faouzi, Godbole, Adwait, Krishna, Shankaranarayanan, Vafeiadis, Viktor
In PLDI'20, Lee et al. introduced the \emph{promising } semantics PS 2.0 of the C++ concurrency that captures most of the common program transformations while satisfying the DRF guarantee. The reachability problem for finite-state programs under PS 2
Externí odkaz:
http://arxiv.org/abs/2007.09944