Mohamed Faouzi Atig

Since June 2018, I am a senior lecturer at the Department of Information Technology, Uppsala University. From June 2014 to May 2018, I was an associate senior lecturer at the Department of Information Technology, Uppsala University. I had also a researcher position at the Department of Information Technology, Uppsala University from March 2012 to May 2018. Previously, I was a Post-doctoral researcher at Uppsala University from July 2010 to March 2012.

In March 2017, I obtained my docent degree (comparable to habilitation) from Uppsala University. In June 2010, I obtained my doctoral degree in Computer Science from the University of Paris Diderot- Paris 7 (France) under the supervision of Ahmed Bouajjani and Tayssir Touili. I obtained my master in engineering from the Tunisia Polytechnic School (Tunisia) in June 2005 and my Master of Science in Computer Science from the University of Paris Diderot- Paris 7 (France) in September 2006.

My research interests broadly span model checking, verification of infinite state systems, weak memory models, and automata theory.

For further details, see my CV

• Project Grant for on the Verification of Consistency Models. Supported by VR (the Swedish Research Council). Funding level 3.58 MSEK. (From 2018 to 2021)

• Project Grant for Juniors Researchers on the Verification of Weak Memory Models. Supported by VR (the Swedish Research Council). Funding level 3.4 MSEK. (From 2013 to 2016)

• Project member for the Verification track in UPMARC, the Uppsala Programming for Multicore Architectures Research Centre. Linnaeus competence centre supported by the Swedish Research Council VR. Total Funding level 60 MSEK. (From 2009 to 2018)

• External Collaborator for the Energy Efficient Control project. Supported by EPSRC, the UK's agency for funding research in engineering anf the physical sciences. Total funding level 429,107 GBP.

• Starting grant. Faculty of Science and Technology, Uppsala University. Total funding level 500.000 SEK

• Project member for the Verification of Concurrent Software. Supported by VR, the Swedish Research Council (Project Grant for Research collaboration India-Sweden). Funding level 0.75 MSEK.

Current PhD Students

• Bui Phi Diep (Main supervisor)
• Amendra Shrestha (co-supervisor)
• Tuan Phong Ngo (Main supervisor)

Former PhD Students

• Carl Leonardsson (co-supervisor)
• Othmane Rezine (co-supervisor)
• Yunyun Zhu (co-supervisor)

Hosted Post-Docs

• C. Aiswarya (2014-2016)

Courses at Uppsala University

Year	Semester	Course
2018	Fall	Algorithms and Data Structures (1DL210)
2018	Fall	Programming Theory (1DL034)
2017	Fall	Programming Theory (1DL034)
2017	Fall	Automata and Logic in IT System Modelling (1DL500)
2016	Fall	Automata and Logic in IT System Modelling (1DL500)
2016	Fall	Algorithms and Data Structures (1DL210)
2015	Fall	Algorithms and Data Structures I (1DL210)
2015	Fall	Programming Theory (1DL034)
2014	Fall	Algorithms and Data Structures I (1DL210)
2014	Fall	Programming Theory (1DL034)
2013	Fall	Algorithms and Data Structures I (1DL210)
2013	Fall	Programming Theory (1DL034)
2012	Fall	Programming Theory (1DL034)
2011	Fall	Programming Theory (1DL034)

Courses at University of Paris Diderot-Paris 7

(Also Available DBLP and Google Scholar)

Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs. Parosh Abdulla, Mohamed Faouzi Atig, Frederik Meyer Bonneland, Sarbojit Das, Bengt Jonsson, Magnus Lång, and Konstantinos Sagonas. In Automated Technology for Verification and Analysis, 21st International Symposium, ATVA 2023, Singapore, Oct. 2023. Proceedings., 2023.

Parameterized Verification under TSO with Data Types. Parosh Abdulla, Mohamed Faouzi Atig, Florian Furbach, Adwait A. Godbole, Yacoub G. Hendi, Shankara N. Krishna, and Stephan Spengler. In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, {TACAS} 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2022, Paris, France, April 22-27, 2023, Proceedings, Part {I}, Lecture Notes in Computer Science, pp 588-606, 2023. (DOI, Fulltext).

Optimal Stateless Model Checking for Causal Consistency. Parosh Abdulla, Mohamed Faouzi Atig, S. Krishna, Ashutosh Gupta, and Omkar Tuppe. In Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, {TACAS} 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2022, Paris, France, April 22-27, 2023, Proceedings, Part {I}, pp 105-125, 2023. (DOI, Fulltext).

Overcoming Memory Weakness with Unified Fairness: Systematic Verification of Liveness in Weak Memory Models. Parosh Abdulla, Mohamed Faouzi Atig, Adwait Godbole, Shankaranarayanan Krishna, and Mihir Vahanwala. In Computer Aided Verification - 35th International Conference, {CAV} 2023, Paris, France, July 17-22, 2023, Proceedings, Part {I}}, Lecture Notes in Computer Science, pp 184-205, 2023. (DOI, Fulltext).

Consistency and Persistency in Program Verification: Challenges and Opportunities. Parosh Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Bengt Jonsson, K. Narayan Kumar, and Prakash Saivasan. In Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, volume 13660 of Lecture Notes in Computer Science, pp 494-510, Springer, 2022. (DOI).

The Computing Journal gratefully acknowledges the editorial work of the scientists listed below on the special issue entitled "SI: NETYS 2019". Mohamed Faouzi Atig. In Computing, volume 104, number 10, pp 2157-2157, Springer, 2022. (DOI, Fulltext).

Verifying Reachability for TSO Programs with Dynamic Thread Creation. Parosh Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. In Networked Systems, NETYS 2022, volume 13464 of Lecture Notes in Computer Science, pp 283-300, Springer, 2022. (DOI).

Probabilistic Total Store Ordering. Parosh Abdulla, Mohamed Faouzi Atig, Raj Aryan Agarwal, Adwait Godbole, and S. Krishna. In Programming Languages And Systems, ESOP 2022, Lecture Notes in Computer Science, pp 317-345, Springer Nature, 2022. (DOI, Fulltext, fulltext:print).

The Decidability of Verification under PS 2.0. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Adwait Godbole, S. Krishna, and Viktor Vafeiadis. In Programming Languages And Systems, ESOP 2021, Lecture Notes in Computer Science, pp 1-29, Springer Nature, 2021. (DOI, Fulltext, fulltext:print).

Solving Not-Substring Constraint with Flat Abstraction. Parosh Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukas Holik, Denghang Hu, Wei-Lun Tsai, Zhillin Wu, and Di-De Yen. In Programming Languages And Systems,  APLAS 2021, Lecture Notes in Computer Science, pp 305-320, Springer Nature, 2021. (DOI).

Deciding Reachability under Persistent x86-TSO. Parosh Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. In Proceedings of the ACM on Programming Languages, volume 5, Association for Computing Machinery (ACM), 2021. (DOI, Fulltext, fulltext:print).

What is decidable under the TSO memory model?. Mohamed Faouzi Atig. In ACM SIGLOG News, volume 7, number 4, pp 4-19, Association for Computing Machinery (ACM), 2020. (DOI).

On the State Reachability Problem for Concurrent Programs Under Power. Parosh Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Egor Derevenetc, Carl Leonardsson, and Roland Meyer. In Networked Systems - 8th International Conference, {NETYS} 2020,  Morocco,  Revised Selected Papers, Lecture Notes in Computer Science, Springer Nature Switzerland AG, 2020.

On the Formalization of Decentralized Contact Tracing Protocols. Parosh Abdulla, Mohamed Faouzi Atig, Giorgio Delzanno, Marco Montali, and Arnaud Sangnier. In Proceedings of the 2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis hosted by the Bolzano Summer of Knowledge 2020 {(BOSK} 2020), September 25, 2020, CEUR Workshop Proceedings, pp 65-70, CEUR-WS.org, 2020. (External link).

On the Separability Problem of String Constraints. Parosh Abdulla, Mohamed Faouzi Atig, Vrunda Dave, and Shankara Narayanan Krishna. In 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference), LIPIcs, pp 16:1-16:19, Dagstuhl, Germany, 2020. (DOI, External link).

Boosting Sequential Consistency Checking Using Saturation. Rachid Zennou, Mohamed Faouzi Atig, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, and Mohammed Erradi. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings, Lecture Notes in Computer Science, pp 360-376, Springer Nature, 2020. (DOI).

Parameterized verification under TSO is PSPACE-complete. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Rojin Rezvan. In Proceedings of the ACM on Programming Languages, volume 4, number POPL, pp 26:1-26:29, Association for Computing Machinery (ACM), New York, NY, USA, 2020. (DOI, Fulltext, fulltext:print).

Efficient Handling of String-Number Conversion. Parosh Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Phi Diep Bui, Julian Dolby, Petr Janku, Hsin-Hung Lin, Lukas Holik, and Wei-Cheng Wu. In PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp 943-957, 2020. (DOI).

Preface to the VECoS 2018 special issue of ISSE. Mohamed Faouzi Atig and Simon Bliudze. In Innovations in Systems and Software Engineering, volume 16, number 2, pp 99-100, SPRINGER LONDON LTD, 2020. (DOI).

Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial). Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan-Phong Ngo. In Networked Systems: 7th International Conference, NETYS 2019, Marrakech, Morocco, June 19–21, 2019, Revised Selected Papers, volume 11704 of Lecture Notes in Computer Science, pp 3-18, Springer Nature, 2019. (DOI).

Optimal stateless model checking for reads-from equivalence under sequential consistency. Parosh Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lång, Tuan-Phong Ngo, and Konstantinos Sagonas. In Proceedings of the ACM on Programming Languages, Association for Computing Machinery (ACM), 2019. (DOI, Fulltext, External link, fulltext:print).

Chain-Free String Constraints. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep, Lukas Holik, and Petr Janku. In Automated Technology for Verification and Analysis, volume 11781 of Lecture Notes in Computer Science, pp 277-293, Springer, 2019. (DOI).

Reachability in database-driven systems with numerical attributes under recency bounding. Parosh Aziz Abdulla, Aiswarya Cyriac, Mohamed Faouzi Atig, and Marco Montali. In PODS '19: Proceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, pp 335-352, ACM Press, 2019. (DOI).

Verification of programs under the release-acquire semantics. Parosh Aziz Abdulla, Jatin Arora, Mohamed Faouzi Atig, and Shankaranarayanan Krishna. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp 1117-1132, Association for Computing Machinery (ACM), 2019. (DOI).

Optimal Stateless Model Checking under the Release-Acquire Semantics. Parosh Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan-Phong Ngo. In Proceedings of the ACM on Programming Languages, volume 2, number OOPSLA, pp 1-29, Association for Computing Machinery (ACM), 2018. (DOI, Fulltext, fulltext:print).

Trau: SMT solver for string constraints. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Phi Diep Bui, Lukas Holik, Ahmed Rezine, and Philipp Rümmer. In Proceedings of the 2018 18th Conference on Formal Methods in Computer Aided Design (FMCAD), IEEE, 2018. (DOI, External link).

Verification of timed asynchronous programs. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Shankara Narayanan Krishna, and Shaan Vaidya. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science: FSTTCS 2018, volume 122 of Leibniz International Proceedings in Informatics, pp 8:1-16, Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2018. (DOI, Fulltext).

Verifying quantitative temporal properties of procedural programs. Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. In 29th International Conference on Concurrency Theory, volume 118 of Leibniz International Proceedings in Informatics, pp 15:1-17, Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2018. (DOI, Fulltext).

Universal safety for timed Petri nets is PSPACE-complete. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, and Patrick Totzke. In 29th International Conference on Concurrency Theory, volume 118 of Leibniz International Proceedings in Informatics, pp 6:1-15, Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2018. (DOI, Fulltext).

Complexity of reachability for data-aware dynamic systems. Parosh Aziz Abdulla, C. Aiswarya, Mohamed Faouzi Atig, Marco Montali, and Othmane Rezine. In Proc. 18th International Conference on Application of Concurrency to System Design, pp 11-20, IEEE Computer Society, 2018. (DOI, Fulltext).

Verification and Evaluation of Computer and Communication Systems. Mohamed Faouzi Atig, Saddek Bensalem, Simon Bliudze, and Bruno Monsuez (eds). Volume 11181 of Lecture Notes in Computer Science, Springer, 2018. (DOI).

Replacing store buffers by load buffers in TSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. In Verification and Evaluation of Computer and Communication Systems, volume 11181 of Lecture Notes in Computer Science, pp 22-28, Springer, 2018. (DOI).

Perfect timed communication is hard. Parosh Abdulla, Mohamed Faouzi Atig, and Shankara Narayanan Krishna. In Formal Modeling and Analysis of Timed Systems, volume 11022 of Lecture Notes in Computer Science, pp 91-107, Springer, 2018. (DOI, Fulltext).

Optimal Stateless Model Checking under the Release-Acquire Semantics. Parosh Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Tuan-Phong Ngo. In SPLASH OOPSLA 2018, Boston, Nov 4-9, 2018, ACM Digital Library, 2018. (External link).

A load-buffer semantics for total store ordering. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. In Logical Methods in Computer Science, volume 14, number 1, 2018. (External link).

Mending fences with self-invalidation and self-downgrade. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Stefanos Kaxiras, Carl Leonardsson, Alberto Ros, and Yunyun Zhu. In Logical Methods in Computer Science, volume 14, number 1, 2018. (External link).

Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete. Mohamed Faouzi Atig, Benedikt Bollig, and Peter Habermehl. In International Journal of Foundations of Computer Science, volume 28, number 8, pp 945-975, 2017. (DOI).

Verification of Asynchronous Programs with Nested Locks. Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11-15, 2017, Kanpur, India, volume 93 of Leibniz International Proceedings in Informatics (LIPIcs), pp 11:1-11:14, Dagstuhl, Germany, 2017.

Parity Games on Bounded Phase Multi-pushdown Systems. Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. In Networked Systems: 5th International Conference, NETYS 2017, Marrakech, Morocco, May 17-19, 2017, Proceedings, volume 10299 of Lecture Notes in Computer Science, pp 272-287, Cham, 2017. (DOI).

On the Upward/Downward Closures of Petri Nets?. Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, and Prakash Saivasan. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017), volume 83 of Leibniz International Proceedings in Informatics (LIPIcs), pp 49:1-49:14, Dagstuhl, Germany, 2017. (DOI, External link).

Data Multi-Pushdown Automata. Parosh Aziz Abdulla, C. Aiswarya, and Mohamed Faouzi Atig. In The 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of Leibniz International Proceedings in Informatics (LIPIcs), pp 38:1-38:17, Dagstuhl, Germany, 2017. (DOI).

Flatten and Conquer: A Framework for Efficient Analysis of String Constraints. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Phi Diep Bui, Lukas Hol?k, Ahmed Rezine, and Philipp Rümmer. In SIGPLAN notices, volume 52, number 6, pp 602-617, 2017. (DOI).

Context-bounded analysis for POWER. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. In Tools and Algorithms for the Construction and Analysis of Systems: Part II, volume 10206 of Lecture Notes in Computer Science, pp 56-74, Springer, 2017. (DOI, External link).

Stateless model checking for TSO and PSO. Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. In Acta Informatica, volume 54, number 8, pp 789-818, 2017. (DOI).

Recency-Bounded Verification of Dynamic Database-Driven Systems. Parosh Aziz Abdulla, Aiswarya Cyriac, Mohamed Faouzi Atig, Marco Montali, and Othmane Rezine. In PODS'16: PROCEEDINGS OF THE 35TH ACM SIGMOD-SIGACT-SIGAI SYMPOSIUM ON PRINCIPLES OF DATABASE SYSTEMS, pp 195-210, 2016. (DOI).

The complexity of regular abstractions of one-counter languages. Mohamed Faouzi Atig, Dmitry Chistikov, Piotr Hofman, K. Narayan Kumar, Prakash Saivasan, and Georg Zetzsche. In Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016), pp 207-216, 2016. (DOI).

Data Communicating Processes with Unreliable Channels. Parosh Aziz Abdulla, Aiswarya Cyriac, and Mohamed Faouzi Atig. In Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016), pp 166-175, 2016. (DOI).

Counter-Example Guided Program Verification. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Phi Diep Bui. In FM 2016: Formal Methods, volume 9995 of Lecture Notes in Computer Science, pp 25-42, Springer, 2016. (DOI).

The benefits of duality in verifying concurrent programs under TSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. In 27th International Conference on Concurrency Theory: CONCUR 2016, volume 59 of Leibniz International Proceedings in Informatics (LIPIcs), pp 5:1-15, Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2016. (DOI, Fulltext, External link).

Stateless model checking for POWER. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. In Computer Aided Verification: Part II, volume 9780 of Lecture Notes in Computer Science, pp 134-156, Springer, 2016. (DOI).

Fencing programs with self-invalidation and self-downgrade. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Stefanos Kaxiras, Carl Leonardsson, Alberto Ros, and Yunyun Zhu. In Formal Techniques for Distributed Objects, Components, and Systems, volume 9688 of Lecture Notes in Computer Science, pp 19-35, Springer, 2016. (DOI).

Acceleration in Multi-PushDown Systems. Mohamed Faouzi Atig, K. Narayan Kumar, and Prakash Saivasan. In Tools and Algorithms for the Construction and Analysis of Systems, volume 9636 of Lecture Notes in Computer Science, pp 698-714, Springer, 2016. (DOI).

Precise and sound automatic fence insertion procedure under PSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Magnus Lång, and Tuan Phong Ngo. In Networked Systems: NETYS 2015, volume 9466 of Lecture Notes in Computer Science, pp 32-47, Springer, 2015. (DOI).

Verification of buffered dynamic register automata. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara, and Othmane Rezine. In Networked Systems: NETYS 2015, volume 9466 of Lecture Notes in Computer Science, pp 15-31, Springer, 2015. (DOI).

What's decidable about availability languages?. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi. In Proc. 35th IARCS Conference on Foundation of Software Technology and Theoretical Computer Science, volume 45 of LIPIcs, pp 192-205, Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2015. (DOI, Fulltext).

Verification of Cache Coherence Protocols wrt. Trace Filters. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Zeinab Ganjei, Ahmed Rezine, and Yunyun Zhu. In Proc. 15th Conference on Formal Methods in Computer-Aided Design, pp 9-16, IEEE, Piscataway, NJ, 2015. (Article).

Norn: An SMT solver for string constraints. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. In Computer Aided Verification: Part I, volume 9206 of Lecture Notes in Computer Science, pp 462-469, Springer, 2015. (DOI).

The Best of Both Worlds: Trading efficiency and optimality in fence insertion for TSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Tuan-Phong Ngo. In Programming Languages and Systems: ESOP 2015, volume 9032 of Lecture Notes in Computer Science, pp 308-332, Springer Berlin/Heidelberg, 2015. (DOI, External link).

Stateless model checking for TSO and PSO. Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. In Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2015, volume 9035 of Lecture Notes in Computer Science, pp 353-367, Springer Berlin/Heidelberg, 2015. (DOI).

MPass: An efficient tool for the analysis of message-passing programs. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jonathan Cederberg, Subham Modi, Othmane Rezine, and Gaurav Saini. In Formal Aspects of Component Software, volume 8997 of Lecture Notes in Computer Science, pp 198-206, Springer, 2015. (DOI).

Adjacent Ordered Multi-Pushdown Systems. Mohamed Faouzi Atig, K. Narayan Kumar, and Prakash Shivasan. In International Journal of Foundations of Computer Science, volume 25, number 8, pp 1083-1096, 2014. (DOI).

On Bounded Reachability Analysis of Shared Memory Systems. Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. In {IARCS} Annual Conference on Foundations of Software Technology and Theoretical Computer Science, {FSTTCS} 2014, December 15-17, 2014, New Delhi, India, 2014.

Zenoness for Timed Pushdown Automata. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jari Stenman. In Proceedings 15th International Workshop on Verification of Infinite-State Systems, {INFINITY} 2013, Hanoi, Vietnam, 14th October 2013., pp -47, 2014. (DOI).

Computing optimal reachability costs in priced dense-timed pushdown automata. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jari Stenman. In Language and Automata Theory and Applications: LATA 2014, volume 8370 of Lecture Notes in Computer Science, pp 62-75, Springer Berlin/Heidelberg, 2014. (DOI).

Context-Bounded Analysis of TSO Systems. Mohamed Faouzi Atig, Ahmed Bouajjani, and Gennaro Parlato. In From Programs to Systems: The Systems perspective in Computing, volume 8415 of Lecture Notes in Computer Science, pp 21-38, Springer, 2014. (DOI).

String Constraints for Verification. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukas Holik, Ahmed Rezine, and Philipp Rümmer. In Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings, pp 150-166, Springer, 2014. (DOI).

Infinite-state energy games. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman, Richard Mayr, K. Narayan Kumar, and Patrick Totzke. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, ACM Press, New York, 2014. (DOI).

Verification of Dynamic Register Automata. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmet Kara, and Othmane Rezine. In Leibniz International Proceedings in Informatics: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2014), 2014. (fulltext:postprint).

Activity profiles in online social media. Mohamed Faouzi Atig, Sofia Cassel, Lisa Kaati, and Amendra Shrestha. In Proc. 6th International Conference on Advances in Social Networks Analysis and Mining, pp 850-855, IEEE Computer Society, 2014. (DOI).

Budget-bounded model-checking pushdown systems. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine, and Jari Stenman. In Formal methods in system design, volume 45, number 2, pp 273-301, 2014. (DOI).

Author recognition in discussion boards. Amendra Shrestha, Lisa Kaati, Sofia Cassel, and Mohamed Faouzi Atig. In National Symposium on Technology and Methodology for Security and Crisis Management, 2013.

Analysis of message passing programs using SMT-solvers. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg. In Automated Technology for Verification and Analysis: ATVA 2013, volume 8172 of Lecture Notes in Computer Science, pp 272-286, Springer Berlin/Heidelberg, 2013. (DOI).

Push-down automata with gap-order constraints. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Giorgio Delzanno, and Andreas Podelski. In Fundamentals of Software Engineering: FSEN 2013, volume 8161 of Lecture Notes in Computer Science, pp 199-216, Springer Berlin/Heidelberg, 2013. (DOI).

Adjacent ordered multi-pushdown systems. Mohamed Faouzi Atig, K. Narayan Kumar, and Prakash Saivasan. In Developments in Language Theory: DLT 2013, volume 7907 of Lecture Notes in Computer Science, pp 58-69, Springer Berlin/Heidelberg, 2013. (DOI).

Verification of Directed Acyclic Ad Hoc Networks. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Othmane Rezine. In Formal Techniques for Distributed Systems: FORTE 2013, volume 7892 of Lecture Notes in Computer Science, pp 193-208, Springer Berlin/Heidelberg, 2013. (DOI, fulltext:postprint).

MEMORAX, a Precise and Sound Tool for Automatic Fence Insertion under TSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. In Tools and Algorithms for the Construction and Analysis of Systems, volume 7795 of Lecture Notes in Computer Science, pp 530-536, Springer Berlin/Heidelberg, 2013. (DOI, fulltext:postprint).

Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding. Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. In Automated Technology for Verification and Analysis: ATVA 2012, volume 7561 of Lecture Notes in Computer Science, pp 152-166, Springer Berlin/Heidelberg, 2012. (DOI).

Multi-Pushdown Systems with Budgets. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Jari Stenman, and Othmane Rezine. In Formal Methods in Computer-Aided Design, pp 24-33, 2012. (External link).

Adding time to pushdown automata. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jari Stenman. In Quantities in Formal Methods: QFM 2012, volume 103 of Electronic Proceedings in Theoretical Computer Science, pp 1-16, 2012. (DOI).

Timed lossy channel systems. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science: FSTTCS 2012, volume 18 of Leibniz International Proceedings in Informatics, pp 374-386, Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2012. (DOI).

Dense-Timed Pushdown Automata. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jari Stenman. In Proc. 27th ACM/IEEE Symposium on Logic in Computer Science, pp 35-44, IEEE Computer Society, 2012. (DOI).

Model-Checking of Ordered Multi-Pushdown Automata. Mohamed Faouzi Atig. In Logical Methods in Computer Science, volume 8, number 3, p 20, 2012. (DOI).

Automatic fence insertion in integer programs via predicate abstraction. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. In Static Analysis, volume 7460 of Lecture Notes in Computer Science, pp 164-180, Springer-Verlag, Berlin, 2012. (DOI).

Detecting fair non-termination in multithreaded programs. Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, and Akash Lal. In Computer Aided Verification, volume 7358 of Lecture Notes in Computer Science, pp 210-227, Springer-Verlag, Berlin, 2012. (fulltext).

Counter-Example Guided Fence Insertion under TSO. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. In Tools and Algorithms for the Construction and Analysis of Systems, volume 7214 of Lecture Notes in Computer Science, pp 204-219, Springer-Verlag, Berlin, 2012. (DOI, fulltext:preprint).

What's decidable about weak memory models?. Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. In Programming Languages and Systems, volume 7211 of Lecture Notes in Computer Science, pp 26-46, Springer Berlin/Heidelberg, 2012. (DOI).

The minimal cost reachability problem in priced timed pushdown systems. Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jari Stenman. In Language and Automata Theory and Applications: 6th International Conference, LATA 2012, A Coruña, Spain, March 5-9, 2012, volume 7183 of Lecture Notes in Computer Science, pp 58-69, Springer-Verlag, Berlin, 2012. (DOI).

Approximating Petri net reachability along context-free traces. Mohamed Faouzi Atig and Pierre Ganty. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science: FSTTCS 2011, volume 13 of Leibniz International Proceedings in Informatics, pp 152-163, Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2011. (DOI, fulltext:postprint).

Context-bounded analysis for concurrent programs with dynamic creation of threads. Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. In Logical Methods in Computer Science, volume 7, number 4, pp 4:1-48, 2011. (DOI).

Getting rid of store-buffers in TSO analysis. Mohamed Faouzi Atig, Ahmed Bouajjani, and Gennaro Parlato. In Computer Aided Verification: CAV 2011, volume 6806 of Lecture Notes in Computer Science, pp 99-115, Springer-Verlag, Berlin, 2011. (DOI).

On Yen's path logic for Petri nets. Mohamed Faouzi Atig and Peter Habermehl. In International Journal of Foundations of Computer Science, volume 22, number 4, pp 783-799, 2011. (DOI).

Verifying parallel programs with dynamic communication structures. Tayssir Touili and Mohamed Faouzi Atig. In Theoretical Computer Science, volume 411, pp 3460-3468, 2010. (DOI).

From multi to single stack automata. Mohamed Faouzi Atig. In CONCUR 2010 – Concurrency Theory, volume 6269 of Lecture Notes in Computer Science, pp 117-131, Springer-Verlag, Berlin, 2010. (DOI).

Global model checking of ordered multi-pushdown systems. Mohamed Faouzi Atig. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science: FSTTCS 2010, volume 8 of Leibniz International Proceedings in Informatics, pp 216-227, Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2010. (DOI).

On the verification problem for weak memory models. Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi. In Proc. 37th ACM Symposium on Principles of Programming Languages, pp 7-18, ACM Press, New York, 2010. (DOI).