| 2025 | CAV | Data-Driven Verification of Procedural Programs with Integer Arrays. | Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl |
| 2025 | CAV | On the Complexity of Checking Mixed Isolation Levels for SQL Transactions. | Ahmed Bouajjani, Constantin Enea, Enrique Romn-Calvo |
| 2023 | CONCUR | On Verifying Concurrent Programs Under Weakly Consistent Models (Invited Talk). | Ahmed Bouajjani |
| 2022 | CAV | Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes. | Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl |
| 2022 | SAS | Automated Synthesis of Asynchronizations. | Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri |
| 2021 | ESOP | Checking Robustness Between Weak Transactional Consistency Models. | Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea |
| 2020 | ATVA | Boosting Sequential Consistency Checking Using Saturation. | Rachid Zennou, Mohamed Faouzi Atig, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi |
| 2020 | VMCAI | Formalizing and Checking Multilevel Consistency. | Ahmed Bouajjani, Constantin Enea, Madhavan Mukund, Ranjal Gautham Shenoy, S. P. Suresh |
| 2019 | CAV | Checking Robustness Against Snapshot Isolation. | Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea |
| 2019 | CAV | Gradual Consistency Checking. | Rachid Zennou, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi |
| 2019 | CONCUR | Robustness Against Transactional Causal Consistency. | Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea |
| 2018 | CAV | On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. | Ahmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer |
| 2018 | CAV | Reasoning About TSO Programs Using Reduction and Abstraction. | Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran |
| 2018 | CONCUR | Verifying Quantitative Temporal Properties of Procedural Programs. | Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan |
| 2018 | VECoS | Replacing Store Buffers by Load Buffers in TSO. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo |
| 2017 | CAV | Proving Linearizability Using Forward Simulations. | Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil |
| 2017 | CONCUR | Checking Linearizability of Concurrent Priority Queues. | Ahmed Bouajjani, Constantin Enea, Chao Wang |
| 2017 | ESOP | Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency. | Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran |
| 2017 | POPL | On verifying causal consistency. | Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza |
| 2017 | SAS | Abstract Semantic Diffing of Evolving Concurrent Programs. | Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri |
| 2017 | TACAS | Context-Bounded Analysis for POWER. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo |
| 2016 | CONCUR | The Benefits of Duality in Verifying Concurrent Programs under TSO. | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo |
| 2015 | FASE | Lazy TSO Reachability. | Ahmed Bouajjani, Georgel Calin, Egor Derevenetc, Roland Meyer |
| 2015 | ICALP | On Reducing Linearizability to State Reachability. | Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza |
| 2015 | POPL | Tractable Refinement Checking for Concurrent Objects. | Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza |
| 2014 | POPL | Verifying eventual consistency of optimistic replication systems. | Ahmed Bouajjani, Constantin Enea, Jad Hamza |
| 2013 | ESOP | Checking and Enforcing Robustness against TSO. | Ahmed Bouajjani, Egor Derevenetc, Roland Meyer |
| 2013 | ESOP | Verifying Concurrent Programs against Sequential Specifications. | Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza |
| 2012 | ATVA | Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding. | Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan |
| 2012 | ATVA | Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data. | Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu |
| 2012 | CAV | Detecting Fair Non-termination in Multithreaded Programs. | Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, Akash Lal |
| 2012 | ESOP | What's Decidable about Weak Memory Models? | Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi |
| 2012 | POPL | Analysis of recursively parallel programs. | Ahmed Bouajjani, Michael Emmi |
| 2012 | TACAS | Bounded Phase Analysis of Message-Passing Programs. | Ahmed Bouajjani, Michael Emmi |
| 2012 | VMCAI | Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data. | Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu |
| 2011 | CAV | Getting Rid of Store-Buffers in TSO Analysis. | Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato |
| 2011 | ICALP | Deciding Robustness against Total Store Ordering. | Ahmed Bouajjani, Roland Meyer, Eike Mhlmann |
| 2011 | PLDI | On inter-procedural analysis of programs with lists and data. | Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu |
| 2011 | SAS | On Sequentializing Concurrent Programs. | Ahmed Bouajjani, Michael Emmi, Gennaro Parlato |
| 2010 | CAV | Invariant Synthesis for Programs Manipulating Lists with Unbounded Data. | Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine, Mihaela Sighireanu |
| 2010 | POPL | On the verification problem for weak memory models. | Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi |
| 2009 | CONCUR | A Logic-Based Framework for Reasoning about Composite Data Structures. | Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu |
| 2009 | TACAS | Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. | Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer |
| 2008 | CAV | Monotonic Abstraction for Programs with Dynamic Memory Heaps. | Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frdric Haziza, Ahmed Rezine |
| 2008 | CONCUR | On the Reachability Analysis of Acyclic Networks of Pushdown Systems. | Mohamed Faouzi Atig, Ahmed Bouajjani, Tayssir Touili |
| 2008 | TACAS | Computing Simulations over Tree Automata. | Parosh Aziz Abdulla, Ahmed Bouajjani, Luks Holk, Lisa Kaati, Toms Vojnar |
| 2008 | TACAS | SDSIrep: A Reputation System Based on SDSI. | Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Dejvuth Suwimonteerabuth |
| 2007 | CAV | Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. | Ahmed Bouajjani, Sverine Fratani, Shaz Qadeer |
| 2007 | FCT | Rewriting Systems with Data. | Ahmed Bouajjani, Peter Habermehl, Yan Jurski, Mihaela Sighireanu |
| 2007 | TACAS | A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes. | Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu |
| 2006 | CAV | Programs with Lists Are Counter Automata. | Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Toms Vojnar |
| 2006 | FOSSACS | A Logic of Reachable Patterns in Linked Data-Structures. | Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani |
| 2006 | SAS | Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. | Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, Toms Vojnar |
| 2005 | CONCUR | Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems. | Ahmed Bouajjani, Markus Mller-Olm, Tayssir Touili |
| 2005 | TACAS | Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. | Ahmed Bouajjani, Peter Habermehl, Pierre Moro, Toms Vojnar |
| 2004 | CAV | Abstract Regular Model Checking. | Ahmed Bouajjani, Peter Habermehl, Toms Vojnar |
| 2003 | CONCUR | Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management. | Ahmed Bouajjani, Peter Habermehl, Toms Vojnar |
| 2003 | CSL | Deciding Monotonic Games. | Parosh Aziz Abdulla, Ahmed Bouajjani, Julien d'Orso |
| 2003 | CSL | Verification of Infinite State Systems (Tutorial). | Ahmed Bouajjani |
| 2003 | POPL | A generic approach to the static analysis of concurrent programs with procedures. | Ahmed Bouajjani, Javier Esparza, Tayssir Touili |
| 2002 | CAV | Extrapolating Tree Transformations. | Ahmed Bouajjani, Tayssir Touili |
| 2001 | CAV | TReX: A Tool for Reachability Analysis of Complex Systems. | Aurore Annichini, Ahmed Bouajjani, Mihaela Sighireanu |
| 2001 | ICALP | Effective Lossy Queue Languages. | Parosh Aziz Abdulla, Luc Boasson, Ahmed Bouajjani |
| 2001 | ICALP | Languages, Rewriting Systems, and Verification of Infinite-State Systems. | Ahmed Bouajjani |
| 2001 | LICS | Perturbed Turing Machines and Hybrid Systems. | Eugene Asarin, Ahmed Bouajjani |
| 2001 | LICS | Permutation Rewriting and Algorithmic Verification. | Ahmed Bouajjani, Anca Muscholl, Tayssir Touili |
| 2001 | MFCS | Automatic Verification of Recursive Procedures with One Integer Parameter. | Ahmed Bouajjani, Peter Habermehl, Richard Mayr |
| 2001 | SAS | Analyzing Fair Parametric Extended Automata. | Ahmed Bouajjani, Aurore Collomb-Annichini, Yassine Lakhnech, Mihaela Sighireanu |
| 2000 | CAV | Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. | Aurore Annichini, Eugene Asarin, Ahmed Bouajjani |
| 2000 | CAV | Regular Model Checking. | Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, Tayssir Touili |
| 1999 | CAV | Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. | Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech |
| 1999 | CAV | Handling Global Conditions in Parameterized System Verification. | Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson |
| 1999 | STACS | Model Checking Lossy Vector Addition Systems. | Ahmed Bouajjani, Richard Mayr |
| 1999 | TACAS | Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol. | Parosh Aziz Abdulla, Aurore Annichini, Ahmed Bouajjani |
| 1998 | CAV | On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels. | Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson |
| 1997 | CONCUR | Reachability Analysis of Pushdown Automata: Application to Model-Checking. | Ahmed Bouajjani, Javier Esparza, Oded Maler |
| 1997 | ICALP | Symbolic Reachability Analysis of FIFO Channel Systems with Nonregular Sets of Configurations (Extended Abstract). | Ahmed Bouajjani, Peter Habermehl |
| 1997 | RTSS | On-the-fly symbolic model checking for real-time systems. | Ahmed Bouajjani, Stavros Tripakis, Sergio Yovine |
| 1996 | CONCUR | Constrained Properties, Semilinear Systems, and Petri Nets. | Ahmed Bouajjani, Peter Habermehl |
| 1995 | CAV | From Duration Calculus To Linear Hybrid Automata. | Ahmed Bouajjani, Yassine Lakhnech, Riadh Robbana |
| 1995 | CAV | Verifying omega-Regular Properties for a Subclass of Linear Hybrid Systems. | Ahmed Bouajjani, Riadh Robbana |
| 1995 | CONCUR | Temporal Logic + Timed Automata: Expressiveness and Decidability. | Ahmed Bouajjani, Yassine Lakhnech |
| 1995 | LICS | On the Verification Problem of Nonregular Properties for Nonregular Processes | Ahmed Bouajjani, Rachid Echahed, Peter Habermehl |
| 1995 | POPL | Verifying Infinite State Processes with Sequential and Parallel Composition. | Ahmed Bouajjani, Rachid Echahed, Peter Habermehl |
| 1994 | CAV | Verification of Context-Free Timed Systems Using Linear Hybrid Observers. | Ahmed Bouajjani, Rachid Echahed, Riadh Robbana |
| 1994 | CONCUR | Verification of Nonregular Temporal Properties for Context-Free Processes. | Ahmed Bouajjani, Rachid Echahed, Riadh Robbana |
| 1993 | LICS | On Model Checking for Real-Time Properties with Durations | Ahmed Bouajjani, Rachid Echahed, Joseph Sifakis |
| 1992 | CAV | Property Preserving Simulations. | Saddek Bensalem, Ahmed Bouajjani, Claire Loiseaux, Joseph Sifakis |
| 1991 | ICALP | Safety for Branching Time Semantics. | Ahmed Bouajjani, Jean-Claude Fernandez, Susanne Graf, Carlos Rodrguez, Joseph Sifakis |
| 1990 | CAV | Minimal Model Generation. | Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs |