Mohamed Faouzi Atig
Professor vid Institutionen för informationsteknologi; Datorteknik
- Telefon:
- 018-471 31 59
- E-post:
- mohamed_faouzi.atig@it.uu.se
- Besöksadress:
- Hus 10, Lägerhyddsvägen 1
- Postadress:
- Box 337
751 05 UPPSALA
- Akademiska meriter:
- Docent
- CV:
- Ladda ned CV
- ORCID:
- 0000-0001-8229-3481
Mer information visas för dig som medarbetare om du loggar in.
Kort presentation
I am a senior lecturer 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.
For more information, please click here
Biografi
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 more information, please click here
Publikationer
Senaste publikationer
- Parameterized Verification under TSO with Data Types (2023)
- 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)
- Probabilistic Total Store Ordering (2022)
Alla publikationer
Artiklar
- 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)
Böcker
Kapitel
Konferenser
- Parameterized Verification under TSO with Data Types (2023)
- 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)
- 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)
