On the Reachability Analysis of Acyclic Networks of Pushdown Systems. - Mohamed Faouzi Atig; Ahmed Bouajjani; Tayssir Touili (CONCUR, 2008)

Emptiness of Multi-pushdown Automata Is 2ETIME-Complete. - Mohamed Faouzi Atig; Benedikt Bollig; Peter Habermehl (Developments in Language Theory, 2008)

Analyzing Asynchronous Programs with Preemption. - Mohamed Faouzi Atig; Ahmed Bouajjani; Tayssir Touili (FSTTCS, 2008)

On the Reachability Problem for Dynamic Networks of Concurrent Pushdown Systems. - Mohamed Faouzi Atig; Ahmed Bouajjani (RP, 2009)

From Multi to Single Stack Automata. - Mohamed Faouzi Atig (CONCUR, 2010)

Global Model Checking of Ordered Multi-Pushdown Systems. - Mohamed Faouzi Atig (FSTTCS, 2010)

On the verification problem for weak memory models. - Mohamed Faouzi Atig; Ahmed Bouajjani; Sebastian Burckhardt; Madanlal Musuvathi (POPL, 2010)

Verifying parallel programs with dynamic communication structures. - Tayssir Touili; Mohamed Faouzi Atig (Theor. Comput. Sci., 2010)

Getting Rid of Store-Buffers in TSO Analysis. - Mohamed Faouzi Atig; Ahmed Bouajjani; Gennaro Parlato (CAV, 2011)

Approximating Petri Net Reachability Along Context-free Traces. - Mohamed Faouzi Atig; Pierre Ganty (FSTTCS, 2011)

Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads - Mohamed Faouzi Atig; Ahmed Bouajjani; Shaz Qadeer (Log. Methods Comput. Sci., 2011)

On Yen's Path Logic for Petri Nets. - Mohamed Faouzi Atig; Peter Habermehl (Int. J. Found. Comput. Sci., 2011)

Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding. - Mohamed Faouzi Atig; Ahmed Bouajjani; K. Narayan Kumar; Prakash Saivasan (ATVA, 2012)

Detecting Fair Non-termination in Multithreaded Programs. - Mohamed Faouzi Atig; Ahmed Bouajjani; Michael Emmi; Akash Lal (CAV, 2012)

What's Decidable about Weak Memory Models? - Mohamed Faouzi Atig; Ahmed Bouajjani; Sebastian Burckhardt; Madanlal Musuvathi (ESOP, 2012)

Multi-pushdown systems with budgets. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Othmane Rezine; Jari Stenman (FMCAD, 2012)

Timed Lossy Channel Systems. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Jonathan Cederberg (FSTTCS, 2012)

The Minimal Cost Reachability Problem in Priced Timed Pushdown Systems. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Jari Stenman (LATA, 2012)

Dense-Timed Pushdown Automata. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Jari Stenman (LICS, 2012)

Automatic Fence Insertion in Integer Programs via Predicate Abstraction. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Carl Leonardsson; Ahmed Rezine (SAS, 2012)

Counter-Example Guided Fence Insertion under TSO. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Carl Leonardsson; Ahmed Rezine (TACAS, 2012)

Model checking Branching-Time Properties of Multi-Pushdown Systems is Hard - Mohamed Faouzi Atig; Ahmed Bouajjani; K. Narayan Kumar; Prakash Saivasan (CoRR, 2012)

Model-Checking of Ordered Multi-Pushdown Automata - Mohamed Faouzi Atig (Log. Methods Comput. Sci., 2012)

Adding Time to Pushdown Automata - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Jari Stenman (QFM, 2012)

Analysis of Message Passing Programs Using SMT-Solvers. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Jonathan Cederberg (ATVA, 2013)

Verification of Directed Acyclic Ad Hoc Networks. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Othmane Rezine (FMOODS/FORTE, 2013)

Push-Down Automata with Gap-Order Constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Giorgio Delzanno; Andreas Podelski (FSEN, 2013)

Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Carl Leonardsson; Ahmed Rezine (TACAS, 2013)

Zenoness for Timed Pushdown Automata. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Jari Stenman (INFINITY, 2013)

Activity profiles in online social media. - Mohamed Faouzi Atig; Sofia Cassel; Lisa Kaati; Amendra Shrestha (ASONAM, 2014)

String Constraints for Verification. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Lukás Holík; Ahmed Rezine; Philipp Rümmer; Jari Stenman (CAV, 2014)

Infinite-state energy games. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Piotr Hofman; Richard Mayr; K. Narayan Kumar; Patrick Totzke (CSL-LICS, 2014)

Context-Bounded Analysis of TSO Systems. - Mohamed Faouzi Atig; Ahmed Bouajjani; Gennaro Parlato (FPS@ETAPS, 2014)

MPass: An Efficient Tool for the Analysis of Message-Passing Programs. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Jonathan Cederberg; Subham Modi; Othmane Rezine; Gaurav Saini (FACS, 2014)

Verification of Dynamic Register Automata. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmet Kara 002; Othmane Rezine (FSTTCS, 2014)

On Bounded Reachability Analysis of Shared Memory Systems. - Mohamed Faouzi Atig; Ahmed Bouajjani; K. Narayan Kumar; Prakash Saivasan (FSTTCS, 2014)

Computing Optimal Reachability Costs in Priced Dense-Timed Pushdown Automata. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Jari Stenman (LATA, 2014)

Budget-bounded model-checking pushdown systems. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Othmane Rezine; Jari Stenman (Formal Methods Syst. Des., 2014)

Adjacent Ordered Multi-Pushdown Systems. - Mohamed Faouzi Atig; K. Narayan Kumar; Prakash Saivasan (Int. J. Found. Comput. Sci., 2014)

Norn: An SMT Solver for String Constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Lukás Holík; Ahmed Rezine; Philipp Rümmer; Jari Stenman (CAV (1), 2015)

The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ngo Tuan Phong (ESOP, 2015)

Verification of Cache Coherence Protocols wrt. Trace Filters. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Zeinab Ganjei; Ahmed Rezine; Yunyun Zhu (FMCAD, 2015)

What's Decidable about Availability Languages?. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Roland Meyer 001; Mehdi Seyed Salehi (FSTTCS, 2015)

Verification of Buffered Dynamic Register Automata. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmet Kara 002; Othmane Rezine (NETYS, 2015)

Precise and Sound Automatic Fence Insertion Procedure under PSO. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Magnus Lång; Tuan Phong Ngo (NETYS, 2015)

Stateless Model Checking for POWER. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Bengt Jonsson 001; Carl Leonardsson (CAV (2), 2016)

The Benefits of Duality in Verifying Concurrent Programs under TSO. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmed Bouajjani; Tuan Phong Ngo (CONCUR, 2016)

Counter-Example Guided Program Verification. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Bui Phi Diep (FM, 2016)

Fencing Programs with Self-Invalidation and Self-Downgrade. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Stefanos Kaxiras; Carl Leonardsson; Alberto Ros 001; Yunyun Zhu (FORTE, 2016)

Data Communicating Processes with Unreliable Channels. - Parosh Aziz Abdulla; C. Aiswarya; Mohamed Faouzi Atig (LICS, 2016)

The complexity of regular abstractions of one-counter languages. - Mohamed Faouzi Atig; Dmitry Chistikov 001; Piotr Hofman; K. Narayan Kumar; Prakash Saivasan; Georg Zetzsche (LICS, 2016)

Recency-Bounded Verification of Dynamic Database-Driven Systems. - Parosh Aziz Abdulla; C. Aiswarya; Mohamed Faouzi Atig; Marco Montali; Othmane Rezine (PODS, 2016)

Acceleration in Multi-PushDown Systems. - Mohamed Faouzi Atig; K. Narayan Kumar; Prakash Saivasan (TACAS, 2016)

Recency-Bounded Verification of Dynamic Database-Driven Systems (Extended Version). - Parosh Aziz Abdulla; C. Aiswarya; Mohamed Faouzi Atig; Marco Montali; Othmane Rezine (CoRR, 2016)

Data Multi-Pushdown Automata. - Parosh Aziz Abdulla; C. Aiswarya; Mohamed Faouzi Atig (CONCUR, 2017)

Verification of Asynchronous Programs with Nested Locks. - Mohamed Faouzi Atig; Ahmed Bouajjani; K. Narayan Kumar; Prakash Saivasan (FSTTCS, 2017)

On the Upward/Downward Closures of Petri Nets. - Mohamed Faouzi Atig; Roland Meyer 001; Sebastian Muskalla; Prakash Saivasan (MFCS, 2017)

Parity Games on Bounded Phase Multi-pushdown Systems. - Mohamed Faouzi Atig; Ahmed Bouajjani; K. Narayan Kumar; Prakash Saivasan (NETYS, 2017)

Flatten and conquer: a framework for efficient analysis of string constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Ahmed Rezine; Philipp Rümmer (PLDI, 2017)

Context-Bounded Analysis for POWER. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmed Bouajjani; Tuan Phong Ngo (TACAS (2), 2017)

Stateless model checking for TSO and PSO. - Parosh Aziz Abdulla; Stavros Aronis; Mohamed Faouzi Atig; Bengt Jonsson 001; Carl Leonardsson; Konstantinos Sagonas (Acta Informatica, 2017)

What is Decidable about Perfect Timed Channels? - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Shankara Narayanan Krishna (CoRR, 2017)

Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete. - Mohamed Faouzi Atig; Benedikt Bollig; Peter Habermehl (Int. J. Found. Comput. Sci., 2017)

Complexity of Reachability for Data-Aware Dynamic Systems. - Parosh Aziz Abdulla; C. Aiswarya; Mohamed Faouzi Atig; Marco Montali; Othmane Rezine (ACSD, 2018)

Universal Safety for Timed Petri Nets is PSPACE-complete. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Radu Ciobanu; Richard Mayr; Patrick Totzke (CONCUR, 2018)

Verifying Quantitative Temporal Properties of Procedural Programs. - Mohamed Faouzi Atig; Ahmed Bouajjani; K. Narayan Kumar; Prakash Saivasan (CONCUR, 2018)

Trau: SMT solver for string constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Ahmed Rezine; Philipp Rümmer (FMCAD, 2018)

Perfect Timed Communication Is Hard. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Shankara Narayanan Krishna (FORMATS, 2018)

Verification of Timed Asynchronous Programs. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Shankara Narayanan Krishna; Shaan Vaidya (FSTTCS, 2018)

Replacing Store Buffers by Load Buffers in TSO. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmed Bouajjani; Tuan Phong Ngo (VECoS, 2018)

A Load-Buffer Semantics for Total Store Ordering. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmed Bouajjani; Tuan Phong Ngo (Log. Methods Comput. Sci., 2018)

Mending Fences with Self-Invalidation and Self-Downgrade. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Stefanos Kaxiras; Carl Leonardsson; Alberto Ros 001; Yunyun Zhu (Log. Methods Comput. Sci., 2018)

Optimal stateless model checking under the release-acquire semantics. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Bengt Jonsson 001; Tuan Phong Ngo (Proc. ACM Program. Lang., 2018)

Chain-Free String Constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Bui Phi Diep; Lukás Holík; Petr Janku (ATVA, 2019)

Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial). - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Bengt Jonsson 001; Tuan Phong Ngo (NETYS, 2019)

Verification of programs under the release-acquire semantics. - Parosh Aziz Abdulla; Jatin Arora 002; Mohamed Faouzi Atig; Shankara Narayanan Krishna (PLDI, 2019)

Reachability in Database-driven Systems with Numerical Attributes under Recency Bounding. - Parosh Aziz Abdulla; C. Aiswarya; Mohamed Faouzi Atig; Marco Montali (PODS, 2019)

Optimal stateless model checking for reads-from equivalence under sequential consistency. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Bengt Jonsson 001; Magnus Lång; Tuan Phong Ngo; Konstantinos Sagonas (Proc. ACM Program. Lang., 2019)

Optimal Stateless Model Checking for Reads-From Equivalence under Sequential Consistency. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Bengt Jonsson 001; Magnus Lång; Tuan Phong Ngo; Konstantinos Sagonas (Zenodo, 2019)

Boosting Sequential Consistency Checking Using Saturation. - Rachid Zennou; Mohamed Faouzi Atig; Ranadeep Biswas; Ahmed Bouajjani; Constantin Enea; Mohammed Erradi (ATVA, 2020)

On the Separability Problem of String Constraints. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Vrunda Dave; Shankara Narayanan Krishna (CONCUR, 2020)

On the State Reachability Problem for Concurrent Programs Under Power. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmed Bouajjani; Egor Derevenetc; Carl Leonardsson; Roland Meyer 001 (NETYS, 2020)

On the Formalization of Decentralized Contact Tracing Protocols. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Giorgio Delzanno; Marco Montali; Arnaud Sangnier (OVERLAY, 2020)

Efficient handling of string-number conversion. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Julian Dolby; Petr Janku; Hsin-Hung Lin; Lukás Holík; Wei-Cheng Wu (PLDI, 2020)

The Decidability of Verification under Promising 2.0. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; Shankaranarayanan Krishna; Viktor Vafeiadis (CoRR, 2020)

Preface to the VECoS 2018 special issue of ISSE. - Mohamed Faouzi Atig; Simon Bliudze (Innov. Syst. Softw. Eng., 2020)

Parameterized verification under TSO is PSPACE-complete. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Rojin Rezvan (Proc. ACM Program. Lang., 2020)

What is decidable under the TSO memory model? - Mohamed Faouzi Atig (ACM SIGLOG News, 2020)

Solving Not-Substring Constraint withFlat Abstraction. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Yu-Fang Chen 001; Bui Phi Diep; Lukás Holík; Denghang Hu; Wei-Lun Tsai; Zhilin Wu; Di-De Yen (APLAS, 2021)

The Decidability of Verification under PS 2.0. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; S. Krishna 004; Viktor Vafeiadis (ESOP, 2021)

Deciding reachability under persistent x86-TSO. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmed Bouajjani; K. Narayan Kumar; Prakash Saivasan (Proc. ACM Program. Lang., 2021)

Consistency and Persistency in Program Verification: Challenges and Opportunities. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmed Bouajjani; Bengt Jonsson 001; K. Narayan Kumar; Prakash Saivasan (Principles of Systems Design, 2022)

Probabilistic Total Store Ordering. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Raj Aryan Agarwal; Adwait Godbole; S. Krishna 004 (ESOP, 2022)

Verifying Reachability for TSO Programs with Dynamic Thread Creation. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmed Bouajjani; K. Narayan Kumar; Prakash Saivasan (NETYS, 2022)

The Computing Journal gratefully acknowledges the editorial work of the scientists listed below on the special issue entitled "S.I. : NETYS 2019". - Mohamed Faouzi Atig (Computing, 2022)

Optimal SMC for Transactional Programs. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ashutosh Gupta; Shankaranarayanan Krishna; Omkar Tuppe (CoRR, 2022)

Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Frederik Meyer Bønneland; Sarbojit Das; Bengt Jonsson 001; Magnus Lång; Konstantinos Sagonas (ATVA, 2023)

Overcoming Memory Weakness with Unified Fairness - Systematic Verification of Liveness in Weak Memory Models. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; Shankaranarayanan Krishna; Mihir Vahanwala (CAV (1), 2023)

Parameterized Verification under TSO with Data Types. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Florian Furbach; Adwait Amit Godbole; Yacoub G. Hendi; Shankara Narayanan Krishna; Stephan Spengler (TACAS (1), 2023)

Optimal Stateless Model Checking for Causal Consistency. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; S. Krishna 004; Ashutosh Gupta; Omkar Tuppe (TACAS (1), 2023)

Overcoming Memory Weakness with Unified Fairness. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; Shankaranarayanan Krishna; Mihir Vahanwala (CoRR, 2023)

Chain-Free String Constraints (Technical Report). - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Bui Phi Diep; Lukás Holík; Petr Janku (CoRR, 2023)

Guiding Word Equation Solving Using Graph Neural Networks. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Julie Cailler; Chencheng Liang; Philipp Rümmer (ATVA, 2024)

Fairness and Liveness Under Weak Consistency. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Adwait Godbole; Shankara Narayanan Krishna; Mihir Vahanwala (Taming the Infinities of Concurrency, 2024)

Parsimonious Optimal Dynamic Partial Order Reduction. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Sarbojit Das; Bengt Jonsson 001; Konstantinos Sagonas (CAV (2), 2024)

Verification under TSO with an infinite Data Domain. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Florian Furbach; Shashwat Garg (TACAS (3), 2024)

Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report). - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Julie Cailler; Chencheng Liang; Philipp Rümmer (CoRR, 2024)

Verification under Intel-x86 with Persistency. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Ahmed Bouajjani; K. Narayan Kumar; Prakash Saivasan (Proc. ACM Program. Lang., 2024)

Artifact: Parsimonious Optimal Dynamic Partial Order Reduction. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Sarbojit Das; Bengt Jonsson 001; Konstantinos Sagonas (Zenodo, 2024)

Artifact: Parsimonious Optimal Dynamic Partial Order Reduction. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Sarbojit Das; Bengt Jonsson 001; Konstantinos Sagonas (Zenodo, 2024)

Guiding Word Equation Solving using Graph Neural Networks. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Julie Cailler; Chencheng Liang; Philipp Rümmer (Zenodo, 2024)

Artifact: Trading Space for Simplicity in Stateless Model Checking. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Sarbojit Das; Bengt Jonsson 001; Konstantinos Sagonas (Zenodo, 2024)

Trading Space for Simplicity in Stateless Model Checking. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Sarbojit Das; Bengt Jonsson 001; Konstantinos Sagonas (Real Time and Such, 2025)

Verification of the Release-Acquire Semantics. - Parosh Aziz Abdulla; Elli Anastasiadi; Mohamed Faouzi Atig; Samuel Grahn (CoRR, 2025)

When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report). - Parosh Aziz Abdulla; Mohamed Faouzi Atig; Julie Cailler; Chencheng Liang; Philipp Rümmer (CoRR, 2025)

Checking Consistency of Event-driven Traces. - Parosh Aziz Abdulla; Mohamed Faouzi Atig; R. Govind; Samuel Grahn; Ramanathan S. Thinniyam (CoRR, 2025)