Zobrazeno 1 - 10
of 88
pro vyhledávání: '"Mohamed Faouzi Atig"'
Autor:
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Stefanos Kaxiras, Carl Leonardsson, Alberto Ros, Yunyun Zhu
Publikováno v:
Logical Methods in Computer Science, Vol Volume 14, Issue 1 (2018)
Cache coherence protocols based on self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory instructio
Externí odkaz:
https://doaj.org/article/312a3fcfaf2148e288118a8328f83217
Publikováno v:
Logical Methods in Computer Science, Vol Volume 14, Issue 1 (2018)
We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These proc
Externí odkaz:
https://doaj.org/article/7ea9fc58bb434f19ab745e50c9296321
We address the satisfiability problem for string constraints that combine relational constraints represented by transducers, word equations, and string length constraints. This problem is undecidable in general. Therefore, we propose a new decidable
Externí odkaz:
http://arxiv.org/abs/2307.03970
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 140, Iss Proc. INFINITY 2013, Pp 35-47 (2014)
Timed pushdown automata are pushdown automata extended with a finite set of real-valued clocks. Additionaly, each symbol in the stack is equipped with a value representing its age. The enabledness of a transition may depend on the values of the clock
Externí odkaz:
https://doaj.org/article/8086d28ed4a04e11bd9998ffbf14c0af
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 103, Iss Proc. QFM 2012, Pp 1-16 (2012)
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 pushdown automata (TPDA). Furthermore, we describe how the reachability pro
Externí odkaz:
https://doaj.org/article/c1e7ba0fcf4344f085e1cbfee2661714
Autor:
Mohamed Faouzi Atig
Publikováno v:
Logical Methods in Computer Science, Vol Volume 8, Issue 3 (2012)
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 pop can only be performed on the first non-empty stack. First, we show
Externí odkaz:
https://doaj.org/article/40434fc75756473d8e85b3175131a825
Publikováno v:
Logical Methods in Computer Science, Vol Volume 7, Issue 4 (2011)
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 explores all behaviors of a concurrent program up to some fixed number o
Externí odkaz:
https://doaj.org/article/bb6b9a9607b342009ef178aa505a5935
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783031308222
We present a framework for efficient stateless model checking (SMC) of concurrent programs under three prominent models of causal consistency, $${\texttt {CCv}}, {\texttt {CM}}, \texttt{CC}$$ CCv , CM , CC . Our approach is based on exploring traces
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8225b4d15fef1c24d84294d39d30885d
https://doi.org/10.1007/978-3-031-30823-9_6
https://doi.org/10.1007/978-3-031-30823-9_6
Autor:
Mohamed Faouzi Atig
Publikováno v:
ACM SIGLOG News. 7:4-19
We consider the verification problem of safety and liveness properties of finite-state programs running under the Total Store Ordering (TSO) memory model.We first review the decidability/complexity results regarding these two problems and then show t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9de45a4d11da5a172409d4d1f5ca5966
https://doi.org/10.1145/3458593.3458595
https://doi.org/10.1145/3458593.3458595
Publikováno v:
Programming Languages and Systems ISBN: 9783030993351
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:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d94cb5dcffd6b6356d2f7d3bee6db455
http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-474198
http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-474198