Mohamed Faouzi Atig

ORCID

Publication Activity (10 Years)

Years Active: 2008-2024
Publications (10 Years): 74

Top Venues

Publications

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach, Shashwat Garg
Verification under TSO with an infinite Data Domain. CoRR (2024)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankara Narayanan Krishna, Mihir Vahanwala
Fairness and Liveness Under Weak Consistency. Taming the Infinities of Concurrency (2024)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach, Shashwat Garg
Verification under TSO with an infinite Data Domain. TACAS (3) (2024)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson, Konstantinos Sagonas
Parsimonious Optimal Dynamic Partial Order Reduction. CAV (2) (2024)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson, Konstantinos Sagonas
Parsimonious Optimal Dynamic Partial Order Reduction. CoRR (2024)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Verification under Intel-x86 with Persistency. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Meyer Bønneland, Sarbojit Das, Bengt Jonsson, Magnus Lång, Konstantinos Sagonas
Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs. ATVA (2023)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna, Ashutosh Gupta, Omkar Tuppe
Optimal Stateless Model Checking for Causal Consistency. TACAS (1) (2023)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankaranarayanan Krishna, Mihir Vahanwala
Overcoming Memory Weakness with Unified Fairness - Systematic Verification of Liveness in Weak Memory Models. CAV (1) (2023)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach, Adwait Amit Godbole, Yacoub G. Hendi, Shankara Narayanan Krishna, Stephan Spengler
Parameterized Verification under TSO with Data Types. TACAS (1) (2023)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep, Lukás Holík, Petr Janku
Chain-Free String Constraints (Technical Report). CoRR (2023)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankaranarayanan Krishna, Mihir Vahanwala
Overcoming Memory Weakness with Unified Fairness. CoRR (2023)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Florian Furbach, Adwait Godbole, Yacoub G. Hendi, Shankara Narayanan Krishna, Stephan Spengler
Parameterized Verification under TSO with Data Types. CoRR (2023)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Meyer Bønneland, Sarbojit Das, Bengt Jonsson, Magnus Lång, Konstantinos Sagonas
Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs. CoRR (2023)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ashutosh Gupta, Shankara Narayanan Krishna, Omkar Tuppe
Optimal SMC for Transactional Programs. CoRR (2022)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Raj Aryan Agarwal, Adwait Godbole, Shankara Narayanan Krishna
Probabilistic Total Store Ordering. ESOP (2022)
Mohamed Faouzi Atig
The Computing Journal gratefully acknowledges the editorial work of the scientists listed below on the special issue entitled "S.I. : NETYS 2019". Computing 104 (10) (2022)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Raj Aryan Agarwal, Adwait Godbole, Krishna Shankara Narayanan
Probabilistic Total Store Ordering. CoRR (2022)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Verifying Reachability for TSO Programs with Dynamic Thread Creation. NETYS (2022)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Bengt Jonsson, K. Narayan Kumar, Prakash Saivasan
Consistency and Persistency in Program Verification: Challenges and Opportunities. Principles of Systems Design (2022)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Deciding reachability under persistent x86-TSO. Proc. ACM Program. Lang. 5 (POPL) (2021)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankara Narayanan Krishna, Viktor Vafeiadis
The Decidability of Verification under PS 2.0. ESOP (2021)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Denghang Hu, Wei-Lun Tsai, Zhilin Wu, Di-De Yen
Solving Not-Substring Constraint withFlat Abstraction. APLAS (2021)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Rojin Rezvan
Parameterized verification under TSO is PSPACE-complete. Proc. ACM Program. Lang. 4 (POPL) (2020)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, Shankara Narayanan Krishna
On the Separability Problem of String Constraints. CoRR (2020)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Egor Derevenetc, Carl Leonardsson, Roland Meyer
On the State Reachability Problem for Concurrent Programs Under Power. NETYS (2020)
Rachid Zennou, Mohamed Faouzi Atig, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi
Boosting Sequential Consistency Checking Using Saturation. ATVA (2020)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Vrunda Dave, Shankara Narayanan Krishna
On the Separability Problem of String Constraints. CONCUR (2020)
Mohamed Faouzi Atig, Simon Bliudze
Preface to the VECoS 2018 special issue of ISSE. Innov. Syst. Softw. Eng. 16 (2) (2020)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Julian Dolby, Petr Janku, Hsin-Hung Lin, Lukás Holík, Wei-Cheng Wu
Efficient handling of string-number conversion. PLDI (2020)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankara Narayanan Krishna, Viktor Vafeiadis
The Decidability of Verification under Promising 2.0. CoRR (2020)
Mohamed Faouzi Atig
What is decidable under the TSO memory model? ACM SIGLOG News 7 (4) (2020)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Giorgio Delzanno, Marco Montali, Arnaud Sangnier
On the Formalization of Decentralized Contact Tracing Protocols. OVERLAY (2020)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep, Lukás Holík, Petr Janku
Chain-Free String Constraints. ATVA (2019)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lång, Tuan Phong Ngo, Konstantinos Sagonas
Optimal stateless model checking for reads-from equivalence under sequential consistency. Proc. ACM Program. Lang. 3 (OOPSLA) (2019)
Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig, Marco Montali
Reachability in Database-driven Systems with Numerical Attributes under Recency Bounding. PODS (2019)
Parosh Aziz Abdulla, Jatin Arora, Mohamed Faouzi Atig, Shankara Narayanan Krishna
Verification of programs under the release-acquire semantics. PLDI (2019)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Tuan Phong Ngo
Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial). NETYS (2019)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Tuan Phong Ngo
Optimal stateless model checking under the release-acquire semantics. Proc. ACM Program. Lang. 2 (OOPSLA) (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
A Load-Buffer Semantics for Total Store Ordering. Log. Methods Comput. Sci. 14 (1) (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna
Perfect Timed Communication Is Hard. FORMATS (2018)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Verifying Quantitative Temporal Properties of Procedural Programs. CONCUR (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
Replacing Store Buffers by Load Buffers in TSO. VECoS (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, Philipp Rümmer
Trau: SMT solver for string constraints. FMCAD (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, Patrick Totzke
Universal Safety for Timed Petri Nets is PSPACE-complete. CoRR (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna, Shaan Vaidya
Verification of Timed Asynchronous Programs. FSTTCS (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Stefanos Kaxiras, Carl Leonardsson, Alberto Ros, Yunyun Zhu
Mending Fences with Self-Invalidation and Self-Downgrade. Log. Methods Comput. Sci. 14 (1) (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, Patrick Totzke
Universal Safety for Timed Petri Nets is PSPACE-complete. CONCUR (2018)
Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig, Marco Montali, Othmane Rezine
Complexity of Reachability for Data-Aware Dynamic Systems. ACSD (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Tuan Phong Ngo
Optimal Stateless Model Checking under the Release-Acquire Semantics. CoRR (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, Philipp Rümmer
Flatten and conquer: a framework for efficient analysis of string constraints. PLDI (2017)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
Context-Bounded Analysis for POWER. CoRR (2017)
Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig
Data Multi-Pushdown Automata. CONCUR (2017)
Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, Prakash Saivasan
On the Upward/Downward Closures of Petri Nets. MFCS (2017)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
The Benefits of Duality in Verifying Concurrent Programs under TSO. CoRR (2017)
Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, Konstantinos Sagonas
Stateless model checking for TSO and PSO. Acta Informatica 54 (8) (2017)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna
What is Decidable about Perfect Timed Channels? CoRR (2017)
Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, Prakash Saivasan
On the Upward/Downward Closures of Petri Nets. CoRR (2017)
Mohamed Faouzi Atig, Benedikt Bollig, Peter Habermehl
Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete. Int. J. Found. Comput. Sci. 28 (8) (2017)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Verification of Asynchronous Programs with Nested Locks. FSTTCS (2017)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Parity Games on Bounded Phase Multi-pushdown Systems. NETYS (2017)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
Context-Bounded Analysis for POWER. TACAS (2) (2017)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson
Stateless Model Checking for POWER. CoRR (2016)
Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, Georg Zetzsche
The complexity of regular abstractions of one-counter languages. LICS (2016)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
The Benefits of Duality in Verifying Concurrent Programs under TSO. CONCUR (2016)
Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, Georg Zetzsche
Complexity of regular abstractions of one-counter languages. CoRR (2016)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Stefanos Kaxiras, Carl Leonardsson, Alberto Ros, Yunyun Zhu
Mending Fences with Self-Invalidation and Self-Downgrade. CoRR (2016)
Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig
Data Communicating Processes with Unreliable Channels. LICS (2016)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Stefanos Kaxiras, Carl Leonardsson, Alberto Ros, Yunyun Zhu
Fencing Programs with Self-Invalidation and Self-Downgrade. FORTE (2016)
Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig, Marco Montali, Othmane Rezine
Recency-Bounded Verification of Dynamic Database-Driven Systems (Extended Version). CoRR (2016)
Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig, Marco Montali, Othmane Rezine
Recency-Bounded Verification of Dynamic Database-Driven Systems. PODS (2016)
Mohamed Faouzi Atig, K. Narayan Kumar, Prakash Saivasan
Acceleration in Multi-PushDown Systems. TACAS (2016)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep
Counter-Example Guided Program Verification. FM (2016)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson
Stateless Model Checking for POWER. CAV (2) (2016)
Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, Konstantinos Sagonas
Stateless Model Checking for TSO and PSO. CoRR (2015)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ngo Tuan Phong
The Best of Both Worlds: Trading Efficiency and Optimality in Fence Insertion for TSO. ESOP (2015)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Zeinab Ganjei, Ahmed Rezine, Yunyun Zhu
Verification of Cache Coherence Protocols wrt. Trace Filters. FMCAD (2015)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Magnus Lång, Tuan Phong Ngo
Precise and Sound Automatic Fence Insertion Procedure under PSO. NETYS (2015)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Roland Meyer, Mehdi Seyed Salehi
What's Decidable about Availability Languages?. FSTTCS (2015)
Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, Konstantinos Sagonas
Stateless Model Checking for TSO and PSO. TACAS (2015)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
Norn: An SMT Solver for String Constraints. CAV (1) (2015)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara, Othmane Rezine
Verification of Buffered Dynamic Register Automata. NETYS (2015)
Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato
Context-Bounded Analysis of TSO Systems. FPS@ETAPS (2014)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
On Bounded Reachability Analysis of Shared Memory Systems. FSTTCS (2014)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara, Othmane Rezine
Verification of Dynamic Register Automata. FSTTCS (2014)
Mohamed Faouzi Atig, Sofia Cassel, Lisa Kaati, Amendra Shrestha
Activity profiles in online social media. ASONAM (2014)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman, Richard Mayr, K. Narayan Kumar, Patrick Totzke
Infinite-state energy games. CSL-LICS (2014)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jonathan Cederberg, Subham Modi, Othmane Rezine, Gaurav Saini
MPass: An Efficient Tool for the Analysis of Message-Passing Programs. FACS (2014)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine, Jari Stenman
Budget-bounded model-checking pushdown systems. Formal Methods Syst. Des. 45 (2) (2014)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, Jari Stenman
String Constraints for Verification. CAV (2014)
Mohamed Faouzi Atig, K. Narayan Kumar, Prakash Saivasan
Adjacent Ordered Multi-Pushdown Systems. Int. J. Found. Comput. Sci. 25 (8) (2014)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jari Stenman
Computing Optimal Reachability Costs in Priced Dense-Timed Pushdown Automata. LATA (2014)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman, Richard Mayr, K. Narayan Kumar, Patrick Totzke
Infinite-State Energy Games. CoRR (2014)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine
Verification of Directed Acyclic Ad Hoc Networks. FMOODS/FORTE (2013)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, Ahmed Rezine
Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO. TACAS (2013)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jari Stenman
Zenoness for Timed Pushdown Automata. INFINITY (2013)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Giorgio Delzanno, Andreas Podelski
Push-Down Automata with Gap-Order Constraints. FSEN (2013)
Mohamed Faouzi Atig, K. Narayan Kumar, Prakash Saivasan
Adjacent Ordered Multi-Pushdown Systems. Developments in Language Theory (2013)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jonathan Cederberg
Analysis of Message Passing Programs Using SMT-Solvers. ATVA (2013)
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi
What's Decidable about Weak Memory Models? ESOP (2012)

Mohamed Faouzi Atig.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Mohamed Faouzi Atig