Mohamed Faouzi Atig
Professor at Department of Information Technology; Division of Computer Systems
- Telephone:
- +46 18 471 31 59
- E-mail:
- mohamed_faouzi.atig@it.uu.se
- Visiting address:
- Hus 10, Lägerhyddsvägen 1
- Postal address:
- Box 337
751 05 UPPSALA
- CV:
- Download CV
- ORCID:
- 0000-0001-8229-3481
More information is available to staff who log in.
Short presentation
I am a professor in computer systems at the Department of Information Technology, Uppsala University. My research interests broadly span model checking, verification of infinite-state systems, weak memory models, and automata theory.
Biography
Since July 2021, I am a professor in computer systems at the Department of Information Technology, Uppsala University. From June 2018 to June 2021, I was a senior lecturer (i.e., associate professor) at the Department of Information Technology, Uppsala University. From June 2014 to May 2018, I was an associate senior lecturer (i.e., assistant professor) 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.
Publications
Recent publications
- Verification under Intel-x86 with Persistency (2024)
- Parsimonious Optimal Dynamic Partial Order Reduction (2024)
- Verification under TSO with an infinite Data Domain (2024)
- Overcoming Memory Weakness with Unified Fairness (2023)
- Optimal Stateless Model Checking for Causal Consistency (2023)
All publications
Articles
- Verification under Intel-x86 with Persistency (2024)
- The Computing Journal gratefully acknowledges the editorial work of the scientists listed below on the special issue entitled "SI (2022)
- Deciding Reachability under Persistent x86-TSO (2021)
- Parameterized verification under TSO is PSPACE-complete (2020)
- What is decidable under the TSO memory model? (2020)
- Preface to the VECoS 2018 special issue of ISSE (2020)
- Optimal stateless model checking for reads-from equivalence under sequential consistency (2019)
- Optimal Stateless Model Checking under the Release-Acquire Semantics (2018)
- A load-buffer semantics for total store ordering (2018)
- Mending fences with self-invalidation and self-downgrade (2018)
- Stateless model checking for TSO and PSO (2017)
- Flatten and Conquer (2017)
- Emptiness of Ordered Multi-Pushdown Automata is 2ETIME-Complete (2017)
- Budget-bounded model-checking pushdown systems (2014)
- Adjacent Ordered Multi-Pushdown Systems (2014)
- Model-Checking of Ordered Multi-Pushdown Automata (2012)
- Context-bounded analysis for concurrent programs with dynamic creation of threads (2011)
- On Yen's path logic for Petri nets (2011)
- Verifying parallel programs with dynamic communication structures (2010)
Books
Chapters
Conferences
- Parsimonious Optimal Dynamic Partial Order Reduction (2024)
- Verification under TSO with an infinite Data Domain (2024)
- Overcoming Memory Weakness with Unified Fairness (2023)
- Optimal Stateless Model Checking for Causal Consistency (2023)
- Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs (2023)
- Parameterized Verification under TSO with Data Types (2023)
- Probabilistic Total Store Ordering (2022)
- Verifying Reachability for TSO Programs with Dynamic Thread Creation (2022)
- Solving Not-Substring Constraint with Flat Abstraction (2021)
- The Decidability of Verification under PS 2.0 (2021)
- On the State Reachability Problem for Concurrent Programs Under Power (2020)
- Efficient Handling of String-Number Conversion (2020)
- On the Separability Problem of String Constraints (2020)
- On the Formalization of Decentralized Contact Tracing Protocols (2020)
- Boosting Sequential Consistency Checking Using Saturation (2020)
- Verification of programs under the release-acquire semantics (2019)
- Dynamic Partial Order Reduction Under the Release-Acquire Semantics (Tutorial) (2019)
- Chain-Free String Constraints (2019)
- Reachability in database-driven systems with numerical attributes under recency bounding (2019)
- Optimal Stateless Model Checking under the Release-Acquire Semantics (2018)
- Perfect timed communication is hard (2018)
- Complexity of reachability for data-aware dynamic systems (2018)
- Replacing store buffers by load buffers in TSO (2018)
- Trau (2018)
- Universal safety for timed Petri nets is PSPACE-complete (2018)
- Verification of timed asynchronous programs (2018)
- Verifying quantitative temporal properties of procedural programs (2018)
- Context-bounded analysis for POWER (2017)
- Parity Games on Bounded Phase Multi-pushdown Systems (2017)
- Verification of Asynchronous Programs with Nested Locks (2017)
- On the Upward/Downward Closures of Petri Nets∗ (2017)
- Data Multi-Pushdown Automata (2017)
- Data Communicating Processes with Unreliable Channels (2016)
- The benefits of duality in verifying concurrent programs under TSO (2016)
- Counter-Example Guided Program Verification (2016)
- Stateless model checking for POWER (2016)
- Fencing programs with self-invalidation and self-downgrade (2016)
- Recency-Bounded Verification of Dynamic Database-Driven Systems (2016)
- The complexity of regular abstractions of one-counter languages (2016)
- Acceleration in Multi-PushDown Systems (2016)
- Stateless model checking for TSO and PSO (2015)
- MPass (2015)
- Norn (2015)
- Verification of Cache Coherence Protocols wrt. Trace Filters (2015)
- Verification of buffered dynamic register automata (2015)
- Precise and sound automatic fence insertion procedure under PSO (2015)
- What's decidable about availability languages? (2015)
- The Best of Both Worlds: Trading efficiency and optimality in fence insertion for TSO (2015)
- String Constraints for Verification (2014)
- Infinite-state energy games (2014)
- Verification of Dynamic Register Automata (2014)
- Zenoness for Timed Pushdown Automata (2014)
- Computing optimal reachability costs in priced dense-timed pushdown automata (2014)
- On Bounded Reachability Analysis of Shared Memory Systems (2014)
- Context-Bounded Analysis of TSO Systems (2014)
- Activity profiles in online social media (2014)
- Analysis of message passing programs using SMT-solvers (2013)
- MEMORAX, a Precise and Sound Tool for Automatic Fence Insertion under TSO (2013)
- Push-down automata with gap-order constraints (2013)
- Verification of Directed Acyclic Ad Hoc Networks (2013)
- Adjacent ordered multi-pushdown systems (2013)
- Author recognition in discussion boards (2013)
- Timed lossy channel systems (2012)
- Counter-Example Guided Fence Insertion under TSO (2012)
- Automatic fence insertion in integer programs via predicate abstraction (2012)
- Adding time to pushdown automata (2012)
- Dense-Timed Pushdown Automata (2012)
- The minimal cost reachability problem in priced timed pushdown systems (2012)
- Multi-Pushdown Systems with Budgets (2012)
- What's decidable about weak memory models? (2012)
- Detecting fair non-termination in multithreaded programs (2012)
- Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding (2012)
- Getting rid of store-buffers in TSO analysis (2011)
- Approximating Petri net reachability along context-free traces (2011)
- Global model checking of ordered multi-pushdown systems (2010)
- From multi to single stack automata (2010)
- On the verification problem for weak memory models (2010)
