Ahmed Bouajjani

198 papers A* 36A 14B 32C 5Journal 58Unranked 50
YearRankTypeTitle / Venue / Authors
2026 J jnl
Parametrised Verification of Intel-x86 Programs.
Proc. ACM Program. Lang.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
2025 — conf
Data-Driven Verification of Procedural Programs with Integer Arrays.
CAV (4)
Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl
2025 J jnl
Data-driven Verification of Procedural Programs with Integer Arrays.
CoRR
Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl
2025 — conf
Enhancing Numerical Invariants Learning with Bounded Reachability Analysis.
NETYS
Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl
2025 — conf
On the Complexity of Checking Mixed Isolation Levels for SQL Transactions.
CAV (4)
Ahmed Bouajjani, Constantin Enea, Enrique Román-Calvo
2025 J jnl
On the Complexity of Checking Mixed Isolation Levels for SQL Transactions.
CoRR
Ahmed Bouajjani, Constantin Enea, Enrique Román-Calvo
2024 — conf
On Verifying Concurrent Programs Under Weak Consistency Models: Decidability and Complexity.
Taming the Infinities of Concurrency
Ahmed Bouajjani
2024 J jnl
Verification under Intel-x86 with Persistency.
Proc. ACM Program. Lang.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
2023 — conf
Comparing Causal Convergence Consistency Models.
NETYS
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
2023 J jnl
Dynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation Levels.
CoRR
Ahmed Bouajjani, Constantin Enea, Enrique Román-Calvo
2023 J jnl
Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels.
Proc. ACM Program. Lang.
Ahmed Bouajjani, Constantin Enea, Enrique Román-Calvo
2023 B conf
On Verifying Concurrent Programs Under Weakly Consistent Models (Invited Talk).
CONCUR
Ahmed Bouajjani
2022 B conf
Automated Synthesis of Asynchronizations.
SAS
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri
2022 J jnl
Automated Synthesis of Asynchronizations.
CoRR
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri
2022 B ed.
Automated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings
ATVA
Ahmed Bouajjani, Lukás Holík, Zhilin Wu
2022 J jnl
Checking causal consistency of distributed databases.
Computing
Rachid Zennou, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi
2022 — conf
Consistency and Persistency in Program Verification: Challenges and Opportunities.
Principles of Systems Design
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Bengt Jonsson, K. Narayan Kumar, Prakash Saivasan
2022 — conf
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes.
CAV (1)
Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl
2022 J jnl
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes.
CoRR
Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl
2022 — conf
Varda: A Framework for Compositional Distributed Programming.
NETYS
Laurent Prosperi, Ahmed Bouajjani, Marc Shapiro
2022 — conf
Verifying Reachability for TSO Programs with Dynamic Thread Creation.
NETYS
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
2021 A conf
Checking Robustness Between Weak Transactional Consistency Models.
ESOP
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
2021 J jnl
Checking Robustness Between Weak Transactional Consistency Models.
CoRR
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
2021 J jnl
Deciding reachability under persistent x86-TSO.
Proc. ACM Program. Lang.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
2021 J jnl
Robustness Against Transactional Causal Consistency.
Log. Methods Comput. Sci.
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
2020 B conf
Boosting Sequential Consistency Checking Using Saturation.
ATVA
Rachid Zennou, Mohamed Faouzi Atig, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi
2020 J jnl
Checking Causal Consistency of Distributed Databases.
CoRR
Rachid Zennou, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi
2020 B conf
Formalizing and Checking Multilevel Consistency.
VMCAI
Ahmed Bouajjani, Constantin Enea, Madhavan Mukund, Ranjal Gautham Shenoy, S. P. Suresh
2020 — conf
On the State Reachability Problem for Concurrent Programs Under Power.
NETYS
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Egor Derevenetc, Carl Leonardsson, Roland Meyer
2019 J jnl
Abstract semantic diffing of evolving concurrent programs.
Formal Methods Syst. Des.
Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri
2019 — conf
Checking Causal Consistency of Distributed Databases.
NETYS
Rachid Zennou, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi
2019 — conf
Checking Robustness Against Snapshot Isolation.
CAV (2)
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
2019 J jnl
Checking Robustness Against Snapshot Isolation.
CoRR
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
2019 J jnl
Editorial, special issue of NETYS 2015.
Computing
Ahmed Bouajjani, Hugues Fauconnier
2019 — conf
Gradual Consistency Checking.
CAV (2)
Rachid Zennou, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi
2019 B conf
Robustness Against Transactional Causal Consistency.
CONCUR
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
2019 J jnl
Robustness Against Transactional Causal Consistency.
CoRR
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
2018 J jnl
A Load-Buffer Semantics for Total Store Ordering.
Log. Methods Comput. Sci.
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
2018 — ch.
Model Checking Procedural Programs.
Handbook of Model Checking
Rajeev Alur, Ahmed Bouajjani, Javier Esparza
2018 — conf
On Verifying TSO Robustness for Event-Driven Asynchronous Programs.
NETYS
Ahmed Bouajjani, Constantin Enea, Madhavan Mukund, Rajarshi Roy
2018 J jnl
On reducing linearizability to state reachability.
Inf. Comput.
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
2018 — conf
On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony.
CAV (2)
Ahmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer
2018 J jnl
On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony.
CoRR
Ahmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer
2018 — conf
Reasoning About TSO Programs Using Reduction and Abstraction.
CAV (2)
Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran
2018 J jnl
Reasoning About TSO Programs Using Reduction and Abstraction.
CoRR
Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran
2018 C conf
Replacing Store Buffers by Load Buffers in TSO.
VECoS
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
2018 B conf
Verifying Quantitative Temporal Properties of Procedural Programs.
CONCUR
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
2017 B conf
Abstract Semantic Diffing of Evolving Concurrent Programs.
SAS
Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri
2017 B conf
Checking Linearizability of Concurrent Priority Queues.
CONCUR
Ahmed Bouajjani, Constantin Enea, Chao Wang
2017 J jnl
Checking Linearizability of Concurrent Priority Queues.
CoRR
Ahmed Bouajjani, Constantin Enea, Chao Wang
2017 — conf
Context-Bounded Analysis for POWER.
TACAS (2)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
2017 J jnl
Context-Bounded Analysis for POWER.
CoRR
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
2017 C ed.
Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FORTE 2017, Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Neuchâtel, Switzerland, June 19-22, 2017, Proceedings
FORTE
Ahmed Bouajjani, Alexandra Silva
2017 A* conf
On verifying causal consistency.
POPL
Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza
2017 — conf
Parity Games on Bounded Phase Multi-pushdown Systems.
NETYS
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
2017 — conf
Proving Linearizability Using Forward Simulations.
CAV (2)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil
2017 J jnl
Proving linearizability using forward simulations.
CoRR
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil
2017 J jnl
The Benefits of Duality in Verifying Concurrent Programs under TSO.
CoRR
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
2017 — conf
Verification of Asynchronous Programs with Nested Locks.
FSTTCS
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
2017 B ed.
Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings
VNCAI
Ahmed Bouajjani, David Monniaux
2017 A conf
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency.
ESOP
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran
2016 J jnl
2014 CAV award announcement.
Formal Methods Syst. Des.
Marta Kwiatkowska, Moshe Y. Vardi, Ahmed Bouajjani, Thomas Ball
2016 J jnl
On Verifying Causal Consistency.
CoRR
Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza
2016 B conf
The Benefits of Duality in Verifying Concurrent Programs under TSO.
CONCUR
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
2015 — conf
Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk).
FSTTCS
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
2015 B conf
Lazy TSO Reachability.
FASE
Ahmed Bouajjani, Georgel Calin, Egor Derevenetc, Roland Meyer
2015 J jnl
Lazy TSO Reachability.
CoRR
Ahmed Bouajjani, Georgel Calin, Egor Derevenetc, Roland Meyer
2015 — ed.
Networked Systems - Third International Conference, NETYS 2015, Agadir, Morocco, May 13-15, 2015, Revised Selected Papers
NETYS
Ahmed Bouajjani, Hugues Fauconnier
2015 — conf
On Reducing Linearizability to State Reachability.
ICALP (2)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
2015 J jnl
On Reducing Linearizability to State Reachability.
CoRR
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
2015 A* conf
Tractable Refinement Checking for Concurrent Objects.
POPL
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
2014 J jnl
Bounded phase analysis of message-passing programs.
Int. J. Softw. Tools Technol. Transf.
Ahmed Bouajjani, Michael Emmi
2014 — conf
Context-Bounded Analysis of TSO Systems.
FPS@ETAPS
Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato
2014 — conf
On Bounded Reachability Analysis of Shared Memory Systems.
FSTTCS
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
2014 C conf
Robustness against Relaxed Memory Models.
Software Engineering
Ahmed Bouajjani, Egor Derevenetc, Roland Meyer
2014 A* conf
Verifying eventual consistency of optimistic replication systems.
POPL
Ahmed Bouajjani, Constantin Enea, Jad Hamza
2013 J jnl
Analysis of Recursively Parallel Programs.
ACM Trans. Program. Lang. Syst.
Ahmed Bouajjani, Michael Emmi
2013 A conf
Checking and Enforcing Robustness against TSO.
ESOP
Ahmed Bouajjani, Egor Derevenetc, Roland Meyer
2013 A conf
Verifying Concurrent Programs against Sequential Specifications.
ESOP
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
2012 B conf
Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data.
VMCAI
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu
2012 J jnl
Abstract regular (tree) model checking.
Int. J. Softw. Tools Technol. Transf.
Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, Tomás Vojnar
2012 B conf
Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data.
ATVA
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu
2012 A* conf
Analysis of recursively parallel programs.
POPL
Ahmed Bouajjani, Michael Emmi
2012 A conf
Bounded Phase Analysis of Message-Passing Programs.
TACAS
Ahmed Bouajjani, Michael Emmi
2012 A* conf
Detecting Fair Non-termination in Multithreaded Programs.
CAV
Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, Akash Lal
2012 J jnl
Editorʼs foreword.
J. Comput. Syst. Sci.
Ahmed Bouajjani, David Harel, Lenore D. Zuck
2012 B conf
Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding.
ATVA
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
2012 J jnl
Model checking Branching-Time Properties of Multi-Pushdown Systems is Hard
CoRR
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
2012 J jnl
Robustness Checking against TSO: Attacks and Defence
CoRR
Ahmed Bouajjani, Egor Derevenetc, Roland Meyer
2012 A conf
What's Decidable about Weak Memory Models?
ESOP
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi
2012 J jnl
Widening techniques for regular tree model checking.
Int. J. Softw. Tools Technol. Transf.
Ahmed Bouajjani, Tayssir Touili
2011 J jnl
Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads
Log. Methods Comput. Sci.
Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer
2011 — conf
Deciding Robustness against Total Store Ordering.
ICALP (2)
Ahmed Bouajjani, Roland Meyer, Eike Möhlmann
2011 A* conf
Getting Rid of Store-Buffers in TSO Analysis.
CAV
Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato
2011 B conf
On Sequentializing Concurrent Programs.
SAS
Ahmed Bouajjani, Michael Emmi, Gennaro Parlato
2011 A* conf
On inter-procedural analysis of programs with lists and data.
PLDI
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu
2011 J jnl
Programs with lists are counter automata.
Formal Methods Syst. Des.
Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar
2010 B ed.
Automated Technology for Verification and Analysis - 8th International Symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings
ATVA
Ahmed Bouajjani, Wei-Ngan Chin
2010 A* conf
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data.
CAV
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine, Mihaela Sighireanu
2010 A* conf
On the verification problem for weak memory models.
POPL
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi
2009 J jnl
A Framework to Handle Linear Temporal Properties in (\omega-)Regular Model Checking
CoRR
Ahmed Bouajjani, Axel Legay, Pierre Wolper
2009 J jnl
A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
Log. Methods Comput. Sci.
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Yan Jurski, Mihaela Sighireanu
2009 B conf
A Logic-Based Framework for Reasoning about Composite Data Structures.
CONCUR
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu
2009 J jnl
Composed Bisimulation for Tree Automata.
Int. J. Found. Comput. Sci.
Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar
2009 A* ed.
Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings
CAV
Ahmed Bouajjani, Oded Maler
2009 A conf
Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads.
TACAS
Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer
2009 — conf
On the Reachability Problem for Dynamic Networks of Concurrent Pushdown Systems.
RP
Mohamed Faouzi Atig, Ahmed Bouajjani
2009 — conf
Rewriting Systems over Nested Data Words.
MEMICS
Ahmed Bouajjani, Cezara Dragoi, Yan Jurski, Mihaela Sighireanu
2008 — conf
Analyzing Asynchronous Programs with Preemption.
FSTTCS
Mohamed Faouzi Atig, Ahmed Bouajjani, Tayssir Touili
2008 C conf
Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata.
CIAA
Ahmed Bouajjani, Peter Habermehl, Lukás Holík, Tayssir Touili, Tomás Vojnar
2008 C conf
Composed Bisimulation for Tree Automata.
CIAA
Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar
2008 A conf
Computing Simulations over Tree Automata.
TACAS
Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar
2008 A* conf
Monotonic Abstraction for Programs with Dynamic Memory Heaps.
CAV
Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ahmed Rezine
2008 J jnl
Monotonic and Downward Closed Games.
J. Log. Comput.
Parosh Aziz Abdulla, Ahmed Bouajjani, Julien d'Orso
2008 B conf
On the Reachability Analysis of Acyclic Networks of Pushdown Systems.
CONCUR
Mohamed Faouzi Atig, Ahmed Bouajjani, Tayssir Touili
2008 A conf
SDSIrep: A Reputation System Based on SDSI.
TACAS
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Dejvuth Suwimonteerabuth
2008 — conf
Shape Analysis via Monotonic Abstraction.
Beyond the Finite: New Challenges in Verification and Semistructured Data
Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ran Ji, Ahmed Rezine
2008 J jnl
Verification of parametric concurrent systems with prioritised FIFO resource management.
Formal Methods Syst. Des.
Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar
2007 A conf
A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes.
TACAS
Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu
2007 J jnl
A Logic of Reachable Patterns in Linked Data-Structures
CoRR
Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani
2007 J jnl
A logic of reachable patterns in linked data-structures.
J. Log. Algebraic Methods Program.
Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani
2007 A* conf
Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures.
CAV
Ahmed Bouajjani, Séverine Fratani, Shaz Qadeer
2007 J jnl
Permutation rewriting and algorithmic verification.
Inf. Comput.
Ahmed Bouajjani, Anca Muscholl, Tayssir Touili
2007 B conf
Rewriting Systems with Data.
FCT
Ahmed Bouajjani, Peter Habermehl, Yan Jurski, Mihaela Sighireanu
2007 J jnl
Symbolic Reachability Analysis of Higher-Order Context-Free Processes
CoRR
Ahmed Bouajjani, Antoine Meyer
2006 — conf
06081 Abstracts Collection -- Software Verification: Infinite-State Model Checking and Static Program Analysis.
Software Verification: Infinite-State Model Checking and Static Program Analysis
Parosh Aziz Abdulla, Ahmed Bouajjani, Markus Müller-Olm
2006 — conf
06081 Executive Summary -- Software Verification: Infinite-State Model Checking and Static Program Analysis.
Software Verification: Infinite-State Model Checking and Static Program Analysis
Parosh Aziz Abdulla, Ahmed Bouajjani, Markus Müller-Olm
2006 B conf
A Logic of Reachable Patterns in Linked Data-Structures.
FoSSaCS
Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani
2006 B conf
Abstract Regular Tree Model Checking of Complex Dynamic Data Structures.
SAS
Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, Tomás Vojnar
2006 — conf
On Symbolic Verification of Weakly Extended PAD.
EXPRESS
Ahmed Bouajjani, Jan Strejcek, Tayssir Touili
2006 J jnl
Parametric Verification of a Group Membership Algorithm.
Theory Pract. Log. Program.
Ahmed Bouajjani, Agathe Merceron
2006 A* conf
Programs with Lists Are Counter Automata.
CAV
Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar
2006 — conf
Reachability analysis of multithreaded software with asynchronous communication.
Software Verification: Infinite-State Model Checking and Static Program Analysis
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejcek
2006 — conf
Rewriting Models of Boolean Programs.
RTA
Ahmed Bouajjani, Javier Esparza
2006 — ed.
Software Verification: Infinite-State Model Checking and Static Program Analysis, 19.02. - 24.02.2006
Software Verification: Infinite-State Model Checking and Static Program Analysis
Parosh Aziz Abdulla, Ahmed Bouajjani, Markus Müller-Olm
2005 — conf
Abstract Regular Tree Model Checking.
INFINITY
Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, Tomás Vojnar
2005 J jnl
Checking Timed Büchi Automata Emptiness Efficiently.
Formal Methods Syst. Des.
Stavros Tripakis, Sergio Yovine, Ahmed Bouajjani
2005 — conf
On Computing Reachability Sets of Process Rewrite Systems.
RTA
Ahmed Bouajjani, Tayssir Touili
2005 J jnl
Parametric Verification of a Group Membership Algorithm
CoRR
Ahmed Bouajjani, Agathe Merceron
2005 — conf
Reachability Analysis of Multithreaded Software with Asynchronous Communication.
FSTTCS
Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejcek
2005 — conf
Regular Model Checking for Programs with Dynamic Memory.
VISSAS
Ahmed Bouajjani
2005 B conf
Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems.
CONCUR
Ahmed Bouajjani, Markus Müller-Olm, Tayssir Touili
2005 A conf
Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking.
TACAS
Ahmed Bouajjani, Peter Habermehl, Pierre Moro, Tomás Vojnar
2004 A* conf
Abstract Regular Model Checking.
CAV
Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar
2004 — conf
Handling Liveness Properties in (
INFINITY
Ahmed Bouajjani, Axel Legay, Pierre Wolper
2004 — conf
Reachability Analysis of Synchronized PA Systems.
INFINITY
Ahmed Bouajjani, Javier Esparza, Tayssir Touili
2004 — conf
Symbolic Reachability Analysis of Higher-Order Context-Free Processes.
FSTTCS
Ahmed Bouajjani, Antoine Meyer
2004 J jnl
Using Forward Reachability Analysis for Verification of Lossy Channel Systems.
Formal Methods Syst. Des.
Parosh Aziz Abdulla, Aurore Collomb-Annichini, Ahmed Bouajjani, Bengt Jonsson
2003 J jnl
A Generic Approach to the Static Analysis of Concurrent Programs with Procedures.
Int. J. Found. Comput. Sci.
Ahmed Bouajjani, Javier Esparza, Tayssir Touili
2003 A* conf
A generic approach to the static analysis of concurrent programs with procedures.
POPL
Ahmed Bouajjani, Javier Esparza, Tayssir Touili
2003 J jnl
Automatic verification of recursive procedures with one integer parameter.
Theor. Comput. Sci.
Ahmed Bouajjani, Peter Habermehl, Richard Mayr
2003 B conf
Deciding Monotonic Games.
CSL
Parosh Aziz Abdulla, Ahmed Bouajjani, Julien d'Orso
2003 — conf
Reachability Analysis of Process Rewrite Systems.
FSTTCS
Ahmed Bouajjani, Tayssir Touili
2003 B conf
Verification of Infinite State Systems (Tutorial).
CSL
Ahmed Bouajjani
2003 B conf
Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management.
CONCUR
Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar
2002 A* conf
Extrapolating Tree Transformations.
CAV
Ahmed Bouajjani, Tayssir Touili
2002 — conf
Parametric Verification of a Group Membership Algorithm.
FTRTFT
Ahmed Bouajjani, Agathe Merceron
2001 B conf
Analyzing Fair Parametric Extended Automata.
SAS
Ahmed Bouajjani, Aurore Collomb-Annichini, Yassine Lakhnech, Mihaela Sighireanu
2001 B conf
Automatic Verification of Recursive Procedures with One Integer Parameter.
MFCS
Ahmed Bouajjani, Peter Habermehl, Richard Mayr
2001 A* conf
Effective Lossy Queue Languages.
ICALP
Parosh Aziz Abdulla, Luc Boasson, Ahmed Bouajjani
2001 A* conf
Languages, Rewriting Systems, and Verification of Infinite-State Systems.
ICALP
Ahmed Bouajjani
2001 A* conf
Permutation Rewriting and Algorithmic Verification.
LICS
Ahmed Bouajjani, Anca Muscholl, Tayssir Touili
2001 A* conf
Perturbed Turing Machines and Hybrid Systems.
LICS
Eugene Asarin, Ahmed Bouajjani
2001 J jnl
Preface.
Theor. Comput. Sci.
Ahmed Bouajjani
2001 A* conf
TReX: A Tool for Reachability Analysis of Complex Systems.
CAV
Aurore Annichini, Ahmed Bouajjani, Mihaela Sighireanu
2000 J jnl
An efficient automata approach to some problems on context-free grammars.
Inf. Process. Lett.
Ahmed Bouajjani, Javier Esparza, Alain Finkel, Oded Maler, Peter Rossmanith, Bernard Willems, Pierre Wolper
2000 A* conf
Regular Model Checking.
CAV
Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, Tayssir Touili
2000 A* conf
Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems.
CAV
Aurore Annichini, Eugene Asarin, Ahmed Bouajjani
1999 A* conf
Handling Global Conditions in Parameterized System Verification.
CAV
Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson
1999 A conf
Model Checking Lossy Vector Addition Systems.
STACS
Ahmed Bouajjani, Richard Mayr
1999 J jnl
Symbolic Reachability Analysis of FIFO-Channel Systems with Nonregular Sets of Configurations.
Theor. Comput. Sci.
Ahmed Bouajjani, Peter Habermehl
1999 A conf
Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol.
TACAS
Parosh Aziz Abdulla, Aurore Annichini, Ahmed Bouajjani
1999 A* conf
Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis.
CAV
Parosh Aziz Abdulla, Aurore Annichini, Saddek Bensalem, Ahmed Bouajjani, Peter Habermehl, Yassine Lakhnech
1998 A* conf
On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels.
CAV
Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson
1997 A conf
On-the-fly symbolic model checking for real-time systems.
RTSS
Ahmed Bouajjani, Stavros Tripakis, Sergio Yovine
1997 B conf
Reachability Analysis of Pushdown Automata: Application to Model-Checking.
CONCUR
Ahmed Bouajjani, Javier Esparza, Oded Maler
1997 A* conf
Symbolic Reachability Analysis of FIFO Channel Systems with Nonregular Sets of Configurations (Extended Abstract).
ICALP
Ahmed Bouajjani, Peter Habermehl
1996 B conf
Constrained Properties, Semilinear Systems, and Petri Nets.
CONCUR
Ahmed Bouajjani, Peter Habermehl
1996 — conf
Model-Checking for Extended Timed Temporal Logics.
FTRTFT
Ahmed Bouajjani, Yassine Lakhnech, Sergio Yovine
1995 A* conf
From Duration Calculus To Linear Hybrid Automata.
CAV
Ahmed Bouajjani, Yassine Lakhnech, Riadh Robbana
1995 — conf
Logics vs. Automata: The Hybrid Case.
Hybrid Systems
Ahmed Bouajjani, Yassine Lakhnech
1995 A* conf
On the Verification Problem of Nonregular Properties for Nonregular Processes
LICS
Ahmed Bouajjani, Rachid Echahed, Peter Habermehl
1995 J jnl
Property Preserving Abstractions for the Verification of Concurrent Systems.
Formal Methods Syst. Des.
Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, Saddek Bensalem
1995 B conf
Temporal Logic + Timed Automata: Expressiveness and Decidability.
CONCUR
Ahmed Bouajjani, Yassine Lakhnech
1995 A* conf
Verifying Infinite State Processes with Sequential and Parallel Composition.
POPL
Ahmed Bouajjani, Rachid Echahed, Peter Habermehl
1995 A* conf
Verifying omega-Regular Properties for a Subclass of Linear Hybrid Systems.
CAV
Ahmed Bouajjani, Riadh Robbana
1994 — conf
On the Automatic Verification of Systems with Continuous Variables and Unbounded Discrete Data Structures.
Hybrid Systems
Ahmed Bouajjani, Rachid Echahed, Riadh Robbana
1994 — conf
Verfying Invariance Properties of Timed Systems with Duration Variables.
FTRTFT
Ahmed Bouajjani, Rachid Echahed, Riadh Robbana
1994 A* conf
Verification of Context-Free Timed Systems Using Linear Hybrid Observers.
CAV
Ahmed Bouajjani, Rachid Echahed, Riadh Robbana
1994 B conf
Verification of Nonregular Temporal Properties for Context-Free Processes.
CONCUR
Ahmed Bouajjani, Rachid Echahed, Riadh Robbana
1993 A* conf
On Model Checking for Real-Time Properties with Durations
LICS
Ahmed Bouajjani, Rachid Echahed, Joseph Sifakis
1992 J jnl
Minimal State Graph Generation.
Sci. Comput. Program.
Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs, Pascal Raymond
1992 A* conf
Property Preserving Simulations.
CAV
Saddek Bensalem, Ahmed Bouajjani, Claire Loiseaux, Joseph Sifakis
1991 A* conf
Safety for Branching Time Semantics.
ICALP
Ahmed Bouajjani, Jean-Claude Fernandez, Susanne Graf, Carlos Rodríguez, Joseph Sifakis
1991 — conf
Verification for Finite Systems (Extended Abstract).
TAPSOFT, Vol.2
Ahmed Bouajjani, Joseph Sifakis
1990 A* conf
Minimal Model Generation.
CAV
Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs
1990 — conf
Minimal Model Generation.
CAV (DIMACS/AMS volume)
Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs
1988 — conf
A logig for the description of behaviours and properties of concurrent systems.
REX Workshop
Ahmed Bouajjani, Susanne Graf, Joseph Sifakis