Ahmed Bouajjani

Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza: Verifying Concurrent Programs against Sequential Specifications. ESOP 2013: 290-309

Ahmed Bouajjani, Egor Derevenetc, Roland Meyer: Checking and Enforcing Robustness against TSO. ESOP 2013: 533-553

Ahmed Bouajjani, David Harel, Lenore D. Zuck: Editorʼs foreword. J. Comput. Syst. Sci. 78(3): 822 (2012)

Ahmed Bouajjani, Tayssir Touili: Widening techniques for regular tree model checking. STTT 14(2): 145-165 (2012)

Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, Tomás Vojnar: Abstract regular (tree) model checking. STTT 14(2): 167-191 (2012)

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan: Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding. ATVA 2012: 152-166

Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu: Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data. ATVA 2012: 167-182

Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, Akash Lal: Detecting Fair Non-termination in Multithreaded Programs. CAV 2012: 210-226

Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi: What's Decidable about Weak Memory Models? ESOP 2012: 26-46

Ahmed Bouajjani, Michael Emmi: Analysis of recursively parallel programs. POPL 2012: 203-214

Ahmed Bouajjani, Michael Emmi: Bounded Phase Analysis of Message-Passing Programs. TACAS 2012: 451-465

Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu: Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data. VMCAI 2012: 1-22

Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan: Model checking Branching-Time Properties of Multi-Pushdown Systems is Hard. CoRR abs/1205.6928 (2012)

Ahmed Bouajjani, Egor Derevenetc, Roland Meyer: Robustness Checking against TSO: Attacks and Defence. CoRR abs/1208.6152 (2012)

Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer: Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads. Logical Methods in Computer Science 7(4) (2011)

Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar: Programs with lists are counter automata. Formal Methods in System Design 38(2): 158-192 (2011)

Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato: Getting Rid of Store-Buffers in TSO Analysis. CAV 2011: 99-115

Ahmed Bouajjani, Roland Meyer, Eike Möhlmann: Deciding Robustness against Total Store Ordering. ICALP (2) 2011: 428-440

Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu: On inter-procedural analysis of programs with lists and data. PLDI 2011: 578-589

Ahmed Bouajjani, Michael Emmi, Gennaro Parlato: On Sequentializing Concurrent Programs. SAS 2011: 129-145

Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine, Mihaela Sighireanu: Invariant Synthesis for Programs Manipulating Lists with Unbounded Data. CAV 2010: 72-88

Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi: On the verification problem for weak memory models. POPL 2010: 7-18

Ahmed Bouajjani, Wei-Ngan Chin (Eds.): Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings. Lecture Notes in Computer Science 6252, Springer 2010, isbn 978-3-642-15642-7

Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Yan Jurski, Mihaela Sighireanu: A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes. Logical Methods in Computer Science 5(2) (2009)

Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar: Composed Bisimulation for Tree Automata. Int. J. Found. Comput. Sci. 20(4): 685-700 (2009)

Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu: A Logic-Based Framework for Reasoning about Composite Data Structures. CONCUR 2009: 178-195

Ahmed Bouajjani, Cezara Dragoi, Yan Jurski, Mihaela Sighireanu: Rewriting Systems over Nested Data Words. MEMICS 2009

Mohamed Faouzi Atig, Ahmed Bouajjani: On the Reachability Problem for Dynamic Networks of Concurrent Pushdown Systems. RP 2009: 1-2

Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer: Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. TACAS 2009: 107-123

Ahmed Bouajjani, Oded Maler (Eds.): Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science 5643, Springer 2009, isbn 978-3-642-02657-7

Ahmed Bouajjani, Axel Legay, Pierre Wolper: A Framework to Handle Linear Temporal Properties in (\omega-)Regular Model Checking. CoRR abs/0901.4080 (2009)

Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar: Verification of parametric concurrent systems with prioritised FIFO resource management. Formal Methods in System Design 32(2): 129-172 (2008)

Parosh Aziz Abdulla, Ahmed Bouajjani, Julien d'Orso: Monotonic and Downward Closed Games. J. Log. Comput. 18(1): 153-169 (2008)

Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ahmed Rezine: Monotonic Abstraction for Programs with Dynamic Memory Heaps. CAV 2008: 341-354

Mohamed Faouzi Atig, Ahmed Bouajjani, Tayssir Touili: On the Reachability Analysis of Acyclic Networks of Pushdown Systems. CONCUR 2008: 356-371

Mohamed Faouzi Atig, Ahmed Bouajjani, Tayssir Touili: Analyzing Asynchronous Programs with Preemption. FSTTCS 2008: 37-48

Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar: Computing Simulations over Tree Automata. TACAS 2008: 93-108

Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Dejvuth Suwimonteerabuth: SDSIrep: A Reputation System Based on SDSI. TACAS 2008: 501-516

Ahmed Bouajjani, Peter Habermehl, Lukás Holík, Tayssir Touili, Tomás Vojnar: Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. CIAA 2008: 57-67

Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar: Composed Bisimulation for Tree Automata. CIAA 2008: 212-222

Ahmed Bouajjani, Jan Strejcek, Tayssir Touili: On Symbolic Verification of Weakly Extended PAD. Electr. Notes Theor. Comput. Sci. 175(3): 47-64 (2007)

Ahmed Bouajjani, Anca Muscholl, Tayssir Touili: Permutation rewriting and algorithmic verification. Inf. Comput. 205(2): 199-224 (2007)

Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani: A logic of reachable patterns in linked data-structures. J. Log. Algebr. Program. 73(1-2): 111-142 (2007)

Ahmed Bouajjani, Séverine Fratani, Shaz Qadeer: Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. CAV 2007: 207-220

Ahmed Bouajjani, Peter Habermehl, Yan Jurski, Mihaela Sighireanu: Rewriting Systems with Data. FCT 2007: 1-22

Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu: A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes. TACAS 2007: 690-705

Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani: A Logic of Reachable Patterns in Linked Data-Structures. CoRR abs/0705.3610 (2007)

Ahmed Bouajjani, Antoine Meyer: Symbolic Reachability Analysis of Higher-Order Context-Free Processes. CoRR abs/0705.3888 (2007)

Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, Tomás Vojnar: Abstract Regular Tree Model Checking. Electr. Notes Theor. Comput. Sci. 149(1): 37-48 (2006)

Ahmed Bouajjani, Agathe Merceron: Parametric Verification of a Group Membership Algorithm. TPLP 6(3): 321-353 (2006)

Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar: Programs with Lists Are Counter Automata. CAV 2006: 517-531

Parosh Aziz Abdulla, Ahmed Bouajjani, Markus Müller-Olm: 06081 Executive Summary -- Software Verification: Infinite-State Model Checking and Static Program Analysis. Software Verification: Infinite-State Model Checking and Static Program Analysis 2006

Parosh Aziz Abdulla, Ahmed Bouajjani, Markus Müller-Olm: 06081 Abstracts Collection -- Software Verification: Infinite-State Model Checking and Static Program Analysis. Software Verification: Infinite-State Model Checking and Static Program Analysis 2006

Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejcek: Reachability analysis of multithreaded software with asynchronous communication. Software Verification: Infinite-State Model Checking and Static Program Analysis 2006

Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani: A Logic of Reachable Patterns in Linked Data-Structures. FoSSaCS 2006: 94-110

Ahmed Bouajjani, Javier Esparza: Rewriting Models of Boolean Programs. RTA 2006: 136-150

Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, Tomás Vojnar: Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. SAS 2006: 52-70

Parosh Aziz Abdulla, Ahmed Bouajjani, Markus Müller-Olm (Eds.): Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02. - 24.02.2006. Dagstuhl Seminar Proceedings 06081, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2006

Ahmed Bouajjani, Axel Legay, Pierre Wolper: Handling Liveness Properties in (omega-)Regular Model Checking. Electr. Notes Theor. Comput. Sci. 138(3): 101-115 (2005)

Ahmed Bouajjani, Javier Esparza, Tayssir Touili: Reachability Analysis of Synchronized PA Systems. Electr. Notes Theor. Comput. Sci. 138(3): 153-178 (2005)

Stavros Tripakis, Sergio Yovine, Ahmed Bouajjani: Checking Timed Büchi Automata Emptiness Efficiently. Formal Methods in System Design 26(3): 267-292 (2005)

Ahmed Bouajjani, Markus Müller-Olm, Tayssir Touili: Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems. CONCUR 2005: 473-487

Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejcek: Reachability Analysis of Multithreaded Software with Asynchronous Communication. FSTTCS 2005: 348-359

Ahmed Bouajjani, Tayssir Touili: On Computing Reachability Sets of Process Rewrite Systems. RTA 2005: 484-499

Ahmed Bouajjani, Peter Habermehl, Pierre Moro, Tomás Vojnar: Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking. TACAS 2005: 13-29

Ahmed Bouajjani: Regular Model Checking for Programs with Dynamic Memory. VISSAS 2005: 17-22

Ahmed Bouajjani, Agathe Merceron: Parametric Verification of a Group Membership Algorithm. CoRR abs/cs/0505033 (2005)

Parosh Aziz Abdulla, Aurore Collomb-Annichini, Ahmed Bouajjani, Bengt Jonsson: Using Forward Reachability Analysis for Verification of Lossy Channel Systems. Formal Methods in System Design 25(1): 39-65 (2004)

Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar: Abstract Regular Model Checking. CAV 2004: 372-386

Ahmed Bouajjani, Antoine Meyer: Symbolic Reachability Analysis of Higher-Order Context-Free Processes. FSTTCS 2004: 135-147

Ahmed Bouajjani, Javier Esparza, Tayssir Touili: A Generic Approach to the Static Analysis of Concurrent Programs with Procedures. Int. J. Found. Comput. Sci. 14(4): 551- (2003)

Ahmed Bouajjani, Peter Habermehl, Richard Mayr: Automatic verification of recursive procedures with one integer parameter. Theor. Comput. Sci. 295: 85-106 (2003)

Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar: Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management. CONCUR 2003: 172-187

Parosh Aziz Abdulla, Ahmed Bouajjani, Julien d'Orso: Deciding Monotonic Games. CSL 2003: 1-14

Ahmed Bouajjani: Verification of Infinite State Systems (Tutorial). CSL 2003: 71

Ahmed Bouajjani, Tayssir Touili: Reachability Analysis of Process Rewrite Systems. FSTTCS 2003: 74-87

Ahmed Bouajjani, Javier Esparza, Tayssir Touili: A generic approach to the static analysis of concurrent programs with procedures. POPL 2003: 62-73

Ahmed Bouajjani, Tayssir Touili: Extrapolating Tree Transformations. CAV 2002: 539-554

Ahmed Bouajjani, Agathe Merceron: Parametric Verification of a Group Membership Algorithm. FTRTFT 2002: 311-330

Ahmed Bouajjani: Preface. Theor. Comput. Sci. 256(1-2): 1-2 (2001)

Aurore Annichini, Ahmed Bouajjani, Mihaela Sighireanu: TReX: A Tool for Reachability Analysis of Complex Systems. CAV 2001: 368-372

Ahmed Bouajjani: Languages, Rewriting Systems, and Verification of Infinite-State Systems. ICALP 2001: 24-39

Parosh Aziz Abdulla, Luc Boasson, Ahmed Bouajjani: Effective Lossy Queue Languages. ICALP 2001: 639-651

Eugene Asarin, Ahmed Bouajjani: Perturbed Turing Machines and Hybrid Systems. LICS 2001: 269-278

Ahmed Bouajjani, Anca Muscholl, Tayssir Touili: Permutation Rewriting and Algorithmic Verification. LICS 2001: 399-408

Ahmed Bouajjani, Peter Habermehl, Richard Mayr: Automatic Verification of Recursive Procedures with One Integer Parameter. MFCS 2001: 198-211

Ahmed Bouajjani, Aurore Collomb-Annichini, Yassine Lakhnech, Mihaela Sighireanu: Analyzing Fair Parametric Extended Automata. SAS 2001: 335-355

Ahmed Bouajjani, Javier Esparza, Alain Finkel, Oded Maler, Peter Rossmanith, Bernard Willems, Pierre Wolper: An efficient automata approach to some problems on context-free grammars. Inf. Process. Lett. 74(5-6): 221-227 (2000)

Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, Tayssir Touili: Regular Model Checking. CAV 2000: 403-418

Aurore Annichini, Eugene Asarin, Ahmed Bouajjani: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. CAV 2000: 419-434

Ahmed Bouajjani, Peter Habermehl: Symbolic Reachability Analysis of FIFO-Channel Systems with Nonregular Sets of Configurations. Theor. Comput. Sci. 221(1-2): 211-250 (1999)

Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson: Handling Global Conditions in Parameterized System Verification. CAV 1999: 134-145

Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech: Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. CAV 1999: 146-159

Ahmed Bouajjani, Richard Mayr: Model Checking Lossy Vector Addition Systems. STACS 1999: 323-333

Parosh Aziz Abdulla, Aurore Annichini, Ahmed Bouajjani: Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol. TACAS 1999: 208-222

Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson: On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels. CAV 1998: 305-318

Ahmed Bouajjani, Javier Esparza, Oded Maler: Reachability Analysis of Pushdown Automata: Application to Model-Checking. CONCUR 1997: 135-150

Ahmed Bouajjani, Peter Habermehl: Symbolic Reachability Analysis of FIFO Channel Systems with Nonregular Sets of Configurations (Extended Abstract). ICALP 1997: 560-570

Ahmed Bouajjani, Stavros Tripakis, Sergio Yovine: On-the-fly symbolic model checking for real-time systems. RTSS 1997: 25-34

Ahmed Bouajjani, Peter Habermehl: Constrained Properties, Semilinear Systems, and Petri Nets. CONCUR 1996: 481-497

Ahmed Bouajjani, Yassine Lakhnech, Sergio Yovine: Model-Checking for Extended Timed Temporal Logics. FTRTFT 1996: 306-326

Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, Saddek Bensalem: Property Preserving Abstractions for the Verification of Concurrent Systems. Formal Methods in System Design 6(1): 11-44 (1995)

Ahmed Bouajjani, Yassine Lakhnech, Riadh Robbana: From Duration Calculus To Linear Hybrid Automata. CAV 1995: 196-210

Ahmed Bouajjani, Riadh Robbana: Verifying omega-Regular Properties for a Subclass of Linear Hybrid Systems. CAV 1995: 437-450

Ahmed Bouajjani, Yassine Lakhnech: Temporal Logic + Timed Automata: Expressiveness and Decidability. CONCUR 1995: 531-545

Ahmed Bouajjani, Yassine Lakhnech: Logics vs. Automata: The Hybrid Case. Hybrid Systems 1995: 531-542

Ahmed Bouajjani, Rachid Echahed, Peter Habermehl: On the Verification Problem of Nonregular Properties for Nonregular Processes. LICS 1995: 123-133

Ahmed Bouajjani, Rachid Echahed, Peter Habermehl: Verifying Infinite State Processes with Sequential and Parallel Composition. POPL 1995: 95-106

Ahmed Bouajjani, Rachid Echahed, Riadh Robbana: Verification of Context-Free Timed Systems Using Linear Hybrid Observers. CAV 1994: 118-131

Ahmed Bouajjani, Rachid Echahed, Riadh Robbana: Verification of Nonregular Temporal Properties for Context-Free Processes. CONCUR 1994: 81-97

Ahmed Bouajjani, Rachid Echahed, Riadh Robbana: Verfying Invariance Properties of Timed Systems with Duration Variables. FTRTFT 1994: 193-210

Ahmed Bouajjani, Rachid Echahed, Riadh Robbana: On the Automatic Verification of Systems with Continuous Variables and Unbounded Discrete Data Structures. Hybrid Systems 1994: 64-85

Ahmed Bouajjani, Rachid Echahed, Joseph Sifakis: On Model Checking for Real-Time Properties with Durations. LICS 1993: 147-159

Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs, Pascal Raymond: Minimal State Graph Generation. Sci. Comput. Program. 18(3): 247-269 (1992)

Saddek Bensalem, Ahmed Bouajjani, Claire Loiseaux, Joseph Sifakis: Property Preserving Simulations. CAV 1992: 260-273

Ahmed Bouajjani, Jean-Claude Fernandez, Susanne Graf, Carlos Rodriguez, Joseph Sifakis: Safety for Branching Time Semantics. ICALP 1991: 76-92

Ahmed Bouajjani, Joseph Sifakis: Verification for Finite Systems (Extended Abstract). TAPSOFT, Vol.2 1991: 55-57

Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs: Minimal Model Generation. CAV 1990: 197-203

Ahmed Bouajjani, Susanne Graf, Joseph Sifakis: A logig for the description of behaviours and properties of concurrent systems. REX Workshop 1988: 398-410