Networked Systems
7th International Conference, NETYS 2019, Marrakech, Morocco, June 19–21, 2019, Revised Selected Papers
Page
%P
56 Result(s)
within
Mohamed Faouzi Atig
-
Chapter and Conference Paper
Verification under TSO with an infinite Data Domain
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 whet...
-
Chapter
Fairness and Liveness Under Weak Consistency
We consider the verification of concurrent programs running on weakly consistent platforms, i.e., weaker semantics than the classical Sequential Consistency (SC) semantics. We describe a framework for the veri...
-
Chapter and Conference Paper
Overcoming Memory Weakness with Unified Fairness
We consider the verification of liveness properties for concurrent programs running on weak memory models. To that end, we identify notions of fairness that preclude demonic non-determinism, are motivated by p...
-
Chapter and Conference Paper
Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs
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, especia...
-
Chapter and Conference Paper
Optimal Stateless Model Checking for Causal Consistency
We present a framework for efficient stateless model checking (SMC) of concurrent programs under three prominent models of causal consistency, ...
-
Article
The Computing Journal gratefully acknowledges the editorial work of the scientists listed below on the special issue entitled “S.I. : NETYS 2019”
-
Chapter and Conference Paper
Verifying Reachability for TSO Programs with Dynamic Thread Creation
The verification of reachability properties for programs under weak memory models is a hard problem, even undecidable in some cases. The decidability of this problem has been investigated so far in the case of...
-
Chapter
Consistency and Persistency in Program Verification: Challenges and Opportunities
We consider the verification of concurrent programs and, in particular, the challenges that arise because modern platforms only guarantee weak semantics, i.e., semantics that are weaker than the classical Sequent...
-
Chapter and Conference Paper
Probabilistic Total Store Ordering
We present 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 Mar...
-
Chapter and Conference Paper
Solving Not-Substring Constraint withFlat Abstraction
Not-substring is currently among the least supported types of string constraints, and existing solvers use only relatively crude heuristics. Yet, not-substring occurs relatively often in practical examples and...
-
Chapter and Conference Paper
On the State Reachability Problem for Concurrent Programs Under Power
We consider the problem of safety verification, formalized as control-state reachability, for concurrent programs running on the Power architecture. Our main result shows that safety verification under Power i...
-
Chapter and Conference Paper
The Decidability of Verification under PS 2.0
We consider the reachability problem for finite-state multi-threaded programs under the promising semantics (PS 2.0) of Lee et al., which captures most common program transformations. Since reachability is alread...
-
Article
Preface to the VECoS 2018 special issue of ISSE
-
Chapter and Conference Paper
Boosting Sequential Consistency Checking Using Saturation
We address the problem of checking that an execution of a shared memory concurrent program is sequentially consistent (SC). This problem is NP-hard due to the necessity of finding a total order between the wr...
-
Book and Conference Proceedings
-
Chapter and Conference Paper
Chain-Free String Constraints
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 genera...
-
Chapter and Conference Paper
Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial)
We describe at a high-level the main concepts in the Release-Acquire (RA) semantics that is part of the C11 language. Furthermore, we describe the ideas behind an optimal dynamic partial order reduction techni...
-
Book and Conference Proceedings
Verification and Evaluation of Computer and Communication Systems
12th International Conference, VECoS 2018, Grenoble, France, September 26–28, 2018, Proceedings
-
Chapter and Conference Paper
Replacing Store Buffers by Load Buffers in TSO
We consider the weak memory model of Total Store Ordering (TSO). In the classical definition of TSO, an unbounded buffer is inserted between each process and the shared memory. The buffers contains pending sto...
-
Chapter and Conference Paper
Perfect Timed Communication Is Hard
We introduce the model of communicating timed automata (CTA) that extends the classical models of finite-state processes communicating through FIFO perfect channels and timed automata, in the sense that the fi...
