Ahmed Bouajjani

ORCID

Publication Activity (10 Years)

Years Active: 1988-2024
Publications (10 Years): 54

Top Venues

Publications

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Verification under Intel-x86 with Persistency. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Ahmed Bouajjani
On Verifying Concurrent Programs Under Weak Consistency Models: Decidability and Complexity. Taming the Infinities of Concurrency (2024)
Ahmed Bouajjani, Constantin Enea, Enrique Román-Calvo
Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Ahmed Bouajjani, Constantin Enea, Enrique Román-Calvo
Dynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation Levels. CoRR (2023)
Ahmed Bouajjani
On Verifying Concurrent Programs Under Weakly Consistent Models (Invited Talk). CONCUR (2023)
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
Comparing Causal Convergence Consistency Models. NETYS (2023)
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri
Automated Synthesis of Asynchronizations. CoRR (2022)
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri
Automated Synthesis of Asynchronizations. SAS (2022)
Rachid Zennou, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi
Checking causal consistency of distributed databases. Computing 104 (10) (2022)
Laurent Prosperi, Ahmed Bouajjani, Marc Shapiro
Varda: A Framework for Compositional Distributed Programming. NETYS (2022)
Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes. CoRR (2022)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Verifying Reachability for TSO Programs with Dynamic Thread Creation. NETYS (2022)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Bengt Jonsson, K. Narayan Kumar, Prakash Saivasan
Consistency and Persistency in Program Verification: Challenges and Opportunities. Principles of Systems Design (2022)
Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes. CAV (1) (2022)
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
Robustness Against Transactional Causal Consistency. Log. Methods Comput. Sci. 17 (1) (2021)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Deciding reachability under persistent x86-TSO. Proc. ACM Program. Lang. 5 (POPL) (2021)
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
Checking Robustness Between Weak Transactional Consistency Models. CoRR (2021)
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
Checking Robustness Between Weak Transactional Consistency Models. ESOP (2021)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Egor Derevenetc, Carl Leonardsson, Roland Meyer
On the State Reachability Problem for Concurrent Programs Under Power. NETYS (2020)
Rachid Zennou, Mohamed Faouzi Atig, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi
Boosting Sequential Consistency Checking Using Saturation. ATVA (2020)
Rachid Zennou, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi
Checking Causal Consistency of Distributed Databases. CoRR (2020)
Ahmed Bouajjani, Constantin Enea, Madhavan Mukund, Gautham Shenoy R., S. P. Suresh
Formalizing and Checking Multilevel Consistency. VMCAI (2020)
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
Robustness Against Transactional Causal Consistency. CoRR (2019)
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
Checking Robustness Against Snapshot Isolation. CoRR (2019)
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
Checking Robustness Against Snapshot Isolation. CAV (2) (2019)
Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea
Robustness Against Transactional Causal Consistency. CONCUR (2019)
Ahmed Bouajjani, Hugues Fauconnier
Editorial, special issue of NETYS 2015. Computing 101 (9) (2019)
Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri
Abstract semantic diffing of evolving concurrent programs. Formal Methods Syst. Des. 54 (1) (2019)
Rachid Zennou, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi
Gradual Consistency Checking. CAV (2) (2019)
Rachid Zennou, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi
Checking Causal Consistency of Distributed Databases. NETYS (2019)
Ahmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer
On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. CAV (2) (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
A Load-Buffer Semantics for Total Store Ordering. Log. Methods Comput. Sci. 14 (1) (2018)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Verifying Quantitative Temporal Properties of Procedural Programs. CONCUR (2018)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
Replacing Store Buffers by Load Buffers in TSO. VECoS (2018)
Ahmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer
On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony. CoRR (2018)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
On reducing linearizability to state reachability. Inf. Comput. 261 (2018)
Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran
Reasoning About TSO Programs Using Reduction and Abstraction. CAV (2) (2018)
Ahmed Bouajjani, Constantin Enea, Madhavan Mukund, Rajarshi Roy
On Verifying TSO Robustness for Event-Driven Asynchronous Programs. NETYS (2018)
Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran
Reasoning About TSO Programs Using Reduction and Abstraction. CoRR (2018)
Ahmed Bouajjani, Constantin Enea, Chao Wang
Checking Linearizability of Concurrent Priority Queues. CONCUR (2017)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency. ESOP (2017)
Ahmed Bouajjani, Constantin Enea, Chao Wang
Checking Linearizability of Concurrent Priority Queues. CoRR (2017)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil
Proving Linearizability Using Forward Simulations. CAV (2) (2017)
Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri
Abstract Semantic Diffing of Evolving Concurrent Programs. SAS (2017)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
Context-Bounded Analysis for POWER. CoRR (2017)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil
Proving linearizability using forward simulations. CoRR (2017)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
The Benefits of Duality in Verifying Concurrent Programs under TSO. CoRR (2017)
Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza
On verifying causal consistency. POPL (2017)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Verification of Asynchronous Programs with Nested Locks. FSTTCS (2017)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Parity Games on Bounded Phase Multi-pushdown Systems. NETYS (2017)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
Context-Bounded Analysis for POWER. TACAS (2) (2017)
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo
The Benefits of Duality in Verifying Concurrent Programs under TSO. CONCUR (2016)
Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza
On Verifying Causal Consistency. CoRR (2016)
Marta Kwiatkowska, Moshe Y. Vardi, Ahmed Bouajjani, Thomas Ball
2014 CAV award announcement. Formal Methods Syst. Des. 48 (3) (2016)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
On Reducing Linearizability to State Reachability. CoRR (2015)
Ahmed Bouajjani, Georgel Calin, Egor Derevenetc, Roland Meyer
Lazy TSO Reachability. CoRR (2015)
Ahmed Bouajjani, Georgel Calin, Egor Derevenetc, Roland Meyer
Lazy TSO Reachability. FASE (2015)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
On Reducing Linearizability to State Reachability. ICALP (2) (2015)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
Tractable Refinement Checking for Concurrent Objects. POPL (2015)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk). FSTTCS (2015)
Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato
Context-Bounded Analysis of TSO Systems. FPS@ETAPS (2014)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
On Bounded Reachability Analysis of Shared Memory Systems. FSTTCS (2014)
Ahmed Bouajjani, Michael Emmi
Bounded phase analysis of message-passing programs. Int. J. Softw. Tools Technol. Transf. 16 (2) (2014)
Ahmed Bouajjani, Constantin Enea, Jad Hamza
Verifying eventual consistency of optimistic replication systems. POPL (2014)
Ahmed Bouajjani, Egor Derevenetc, Roland Meyer
Robustness against Relaxed Memory Models. Software Engineering (2014)
Ahmed Bouajjani, Michael Emmi
Analysis of Recursively Parallel Programs. ACM Trans. Program. Lang. Syst. 35 (3) (2013)
Ahmed Bouajjani, Egor Derevenetc, Roland Meyer
Checking and Enforcing Robustness against TSO. ESOP (2013)
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza
Verifying Concurrent Programs against Sequential Specifications. ESOP (2013)
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi
What's Decidable about Weak Memory Models? ESOP (2012)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Model checking Branching-Time Properties of Multi-Pushdown Systems is Hard CoRR (2012)
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan
Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding. ATVA (2012)
Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, Tomás Vojnar
Abstract regular (tree) model checking. Int. J. Softw. Tools Technol. Transf. 14 (2) (2012)
Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, Akash Lal
Detecting Fair Non-termination in Multithreaded Programs. CAV (2012)
Ahmed Bouajjani, Tayssir Touili
Widening techniques for regular tree model checking. Int. J. Softw. Tools Technol. Transf. 14 (2) (2012)
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu
Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data. ATVA (2012)
Ahmed Bouajjani, Michael Emmi
Bounded Phase Analysis of Message-Passing Programs. TACAS (2012)
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu
Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data. VMCAI (2012)
Ahmed Bouajjani, Michael Emmi
Analysis of recursively parallel programs. POPL (2012)
Ahmed Bouajjani, David Harel, Lenore D. Zuck
Editorʼs foreword. J. Comput. Syst. Sci. 78 (3) (2012)
Ahmed Bouajjani, Egor Derevenetc, Roland Meyer
Robustness Checking against TSO: Attacks and Defence CoRR (2012)
Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar
Programs with lists are counter automata. Formal Methods Syst. Des. 38 (2) (2011)
Ahmed Bouajjani, Roland Meyer, Eike Möhlmann
Deciding Robustness against Total Store Ordering. ICALP (2) (2011)
Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato
Getting Rid of Store-Buffers in TSO Analysis. CAV (2011)
Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer
Context-Bounded Analysis For Concurrent Programs With Dynamic Creation of Threads Log. Methods Comput. Sci. 7 (4) (2011)
Ahmed Bouajjani, Michael Emmi, Gennaro Parlato
On Sequentializing Concurrent Programs. SAS (2011)
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu
On inter-procedural analysis of programs with lists and data. PLDI (2011)
Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi
On the verification problem for weak memory models. POPL (2010)
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine, Mihaela Sighireanu
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data. CAV (2010)
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Yan Jurski, Mihaela Sighireanu
A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes Log. Methods Comput. Sci. 5 (2) (2009)
Mohamed Faouzi Atig, Ahmed Bouajjani
On the Reachability Problem for Dynamic Networks of Concurrent Pushdown Systems. RP (2009)
Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer
Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. TACAS (2009)
Ahmed Bouajjani, Cezara Dragoi, Yan Jurski, Mihaela Sighireanu
Rewriting Systems over Nested Data Words. MEMICS (2009)
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu
A Logic-Based Framework for Reasoning about Composite Data Structures. CONCUR (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) (2009)
Ahmed Bouajjani, Axel Legay, Pierre Wolper
A Framework to Handle Linear Temporal Properties in (\omega-)Regular Model Checking CoRR (2009)
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)
Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ran Ji, Ahmed Rezine
Shape Analysis via Monotonic Abstraction. Beyond the Finite: New Challenges in Verification and Semistructured Data (2008)
Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar
Verification of parametric concurrent systems with prioritised FIFO resource management. Formal Methods Syst. Des. 32 (2) (2008)
Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar
Computing Simulations over Tree Automata. TACAS (2008)
Mohamed Faouzi Atig, Ahmed Bouajjani, Tayssir Touili
On the Reachability Analysis of Acyclic Networks of Pushdown Systems. CONCUR (2008)

Ahmed Bouajjani.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Ahmed Bouajjani