default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDAhmed Bouajjani
Person information
- affiliation: University Paris Diderot (Paris 7), France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
Journal Articles
- 2024
[j33]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): 1189-1212 (2024)- 2023
- [j32]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): 565-590 (2023) - 2022
- [j31]Rachid Zennou, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi:
Checking causal consistency of distributed databases. Computing 104(10): 2181-2201 (2022) - 2021
- [j30]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea:
Robustness Against Transactional Causal Consistency. Log. Methods Comput. Sci. 17(1) (2021) - [j29]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): 1-32 (2021) - 2019
- [j28]Ahmed Bouajjani, Hugues Fauconnier:
Editorial, special issue of NETYS 2015. Computing 101(9): 1225-1226 (2019) - [j27]Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri:
Abstract semantic diffing of evolving concurrent programs. Formal Methods Syst. Des. 54(1): 4-26 (2019) - 2018
- [j26]Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza:
On reducing linearizability to state reachability. Inf. Comput. 261: 383-400 (2018) - [j25]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) - 2016
- [j24]Marta Kwiatkowska, Moshe Y. Vardi, Ahmed Bouajjani, Thomas Ball:
2014 CAV award announcement. Formal Methods Syst. Des. 48(3): 149-151 (2016) - 2014
- [j23]Ahmed Bouajjani, Michael Emmi:
Bounded phase analysis of message-passing programs. Int. J. Softw. Tools Technol. Transf. 16(2): 127-146 (2014) - 2013
- [j22]Ahmed Bouajjani, Michael Emmi:
Analysis of Recursively Parallel Programs. ACM Trans. Program. Lang. Syst. 35(3): 10:1-10:49 (2013) - 2012
- [j21]Ahmed Bouajjani, David Harel, Lenore D. Zuck:
Editorʼs foreword. J. Comput. Syst. Sci. 78(3): 822 (2012) - [j20]Ahmed Bouajjani, Tayssir Touili:
Widening techniques for regular tree model checking. Int. J. Softw. Tools Technol. Transf. 14(2): 145-165 (2012) - [j19]Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, Tomás Vojnar:
Abstract regular (tree) model checking. Int. J. Softw. Tools Technol. Transf. 14(2): 167-191 (2012) - 2011
- [j18]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) - [j17]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): 158-192 (2011) - 2009
- [j16]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) - [j15]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) - 2008
- [j14]Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar:
Verification of parametric concurrent systems with prioritised FIFO resource management. Formal Methods Syst. Des. 32(2): 129-172 (2008) - [j13]Parosh Aziz Abdulla, Ahmed Bouajjani, Julien d'Orso:
Monotonic and Downward Closed Games. J. Log. Comput. 18(1): 153-169 (2008) - 2007
- [j12]Ahmed Bouajjani, Anca Muscholl, Tayssir Touili:
Permutation rewriting and algorithmic verification. Inf. Comput. 205(2): 199-224 (2007) - [j11]Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani:
A logic of reachable patterns in linked data-structures. J. Log. Algebraic Methods Program. 73(1-2): 111-142 (2007) - 2006
- [j10]Ahmed Bouajjani, Agathe Merceron:
Parametric Verification of a Group Membership Algorithm. Theory Pract. Log. Program. 6(3): 321-353 (2006) - 2005
- [j9]Stavros Tripakis, Sergio Yovine, Ahmed Bouajjani:
Checking Timed Büchi Automata Emptiness Efficiently. Formal Methods Syst. Des. 26(3): 267-292 (2005) - 2004
- [j8]Parosh Aziz Abdulla, Aurore Collomb-Annichini, Ahmed Bouajjani, Bengt Jonsson:
Using Forward Reachability Analysis for Verification of Lossy Channel Systems. Formal Methods Syst. Des. 25(1): 39-65 (2004) - 2003
- [j7]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) - [j6]Ahmed Bouajjani, Peter Habermehl, Richard Mayr:
Automatic verification of recursive procedures with one integer parameter. Theor. Comput. Sci. 295: 85-106 (2003) - 2001
- [j5]Ahmed Bouajjani:
Preface. Theor. Comput. Sci. 256(1-2): 1-2 (2001) - 2000
- [j4]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) - 1999
- [j3]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) - 1995
- [j2]Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, Saddek Bensalem:
Property Preserving Abstractions for the Verification of Concurrent Systems. Formal Methods Syst. Des. 6(1): 11-44 (1995) - 1992
- [j1]Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs, Pascal Raymond:
Minimal State Graph Generation. Sci. Comput. Program. 18(3): 247-269 (1992)
Conference and Workshop Papers
- 2024
- [c125]Ahmed Bouajjani:
On Verifying Concurrent Programs Under Weak Consistency Models: Decidability and Complexity. Taming the Infinities of Concurrency 2024: 133-147 - 2023
- [c124]Ahmed Bouajjani:
On Verifying Concurrent Programs Under Weakly Consistent Models (Invited Talk). CONCUR 2023: 2:1-2:1 - [c123]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea:
Comparing Causal Convergence Consistency Models. NETYS 2023: 62-77 - 2022
- [c122]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: 494-510 - [c121]Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl:
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes. CAV (1) 2022: 282-303 - [c120]Laurent Prosperi, Ahmed Bouajjani, Marc Shapiro:
Varda: A Framework for Compositional Distributed Programming. NETYS 2022: 16-30 - [c119]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan:
Verifying Reachability for TSO Programs with Dynamic Thread Creation. NETYS 2022: 283-300 - [c118]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri:
Automated Synthesis of Asynchronizations. SAS 2022: 135-159 - 2021
- [c117]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea:
Checking Robustness Between Weak Transactional Consistency Models. ESOP 2021: 87-117 - 2020
- [c116]Rachid Zennou, Mohamed Faouzi Atig, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi:
Boosting Sequential Consistency Checking Using Saturation. ATVA 2020: 360-376 - [c115]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: 47-59 - [c114]Ahmed Bouajjani, Constantin Enea, Madhavan Mukund, Ranjal Gautham Shenoy, S. P. Suresh:
Formalizing and Checking Multilevel Consistency. VMCAI 2020: 379-400 - 2019
- [c113]Rachid Zennou, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi:
Gradual Consistency Checking. CAV (2) 2019: 267-285 - [c112]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea:
Checking Robustness Against Snapshot Isolation. CAV (2) 2019: 286-304 - [c111]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea:
Robustness Against Transactional Causal Consistency. CONCUR 2019: 30:1-30:18 - [c110]Rachid Zennou, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi:
Checking Causal Consistency of Distributed Databases. NETYS 2019: 35-51 - 2018
- [c109]Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran:
Reasoning About TSO Programs Using Reduction and Abstraction. CAV (2) 2018: 336-353 - [c108]Ahmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer:
On the Completeness of Verifying Message Passing Programs Under Bounded Asynchrony. CAV (2) 2018: 372-391 - [c107]Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan:
Verifying Quantitative Temporal Properties of Procedural Programs. CONCUR 2018: 15:1-15:17 - [c106]Ahmed Bouajjani, Constantin Enea, Madhavan Mukund, Rajarshi Roy:
On Verifying TSO Robustness for Event-Driven Asynchronous Programs. NETYS 2018: 225-239 - [c105]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo:
Replacing Store Buffers by Load Buffers in TSO. VECoS 2018: 22-28 - 2017
- [c104]Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil:
Proving Linearizability Using Forward Simulations. CAV (2) 2017: 542-563 - [c103]Ahmed Bouajjani, Constantin Enea, Chao Wang:
Checking Linearizability of Concurrent Priority Queues. CONCUR 2017: 16:1-16:16 - [c102]Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, Serdar Tasiran:
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency. ESOP 2017: 170-200 - [c101]Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan:
Verification of Asynchronous Programs with Nested Locks. FSTTCS 2017: 11:1-11:14 - [c100]Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan:
Parity Games on Bounded Phase Multi-pushdown Systems. NETYS 2017: 272-287 - [c99]Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza:
On verifying causal consistency. POPL 2017: 626-638 - [c98]Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri:
Abstract Semantic Diffing of Evolving Concurrent Programs. SAS 2017: 46-65 - [c97]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo:
Context-Bounded Analysis for POWER. TACAS (2) 2017: 56-74 - 2016
- [c96]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo:
The Benefits of Duality in Verifying Concurrent Programs under TSO. CONCUR 2016: 5:1-5:15 - 2015
- [c95]Ahmed Bouajjani, Georgel Calin, Egor Derevenetc, Roland Meyer:
Lazy TSO Reachability. FASE 2015: 267-282 - [c94]Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza:
Checking Correctness of Concurrent Objects: Tractable Reductions to Reachability (Invited Talk). FSTTCS 2015: 2-4 - [c93]Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza:
On Reducing Linearizability to State Reachability. ICALP (2) 2015: 95-107 - [c92]Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza:
Tractable Refinement Checking for Concurrent Objects. POPL 2015: 651-662 - 2014
- [c91]Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato:
Context-Bounded Analysis of TSO Systems. FPS@ETAPS 2014: 21-38 - [c90]Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan:
On Bounded Reachability Analysis of Shared Memory Systems. FSTTCS 2014: 611-623 - [c89]Ahmed Bouajjani, Constantin Enea, Jad Hamza:
Verifying eventual consistency of optimistic replication systems. POPL 2014: 285-296 - [c88]Ahmed Bouajjani, Egor Derevenetc, Roland Meyer:
Robustness against Relaxed Memory Models. Software Engineering 2014: 85-86 - 2013
- [c87]Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza:
Verifying Concurrent Programs against Sequential Specifications. ESOP 2013: 290-309 - [c86]Ahmed Bouajjani, Egor Derevenetc, Roland Meyer:
Checking and Enforcing Robustness against TSO. ESOP 2013: 533-553 - 2012
- [c85]Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan:
Linear-Time Model-Checking for Multithreaded Programs under Scope-Bounding. ATVA 2012: 152-166 - [c84]Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu:
Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data. ATVA 2012: 167-182 - [c83]Mohamed Faouzi Atig, Ahmed Bouajjani, Michael Emmi, Akash Lal:
Detecting Fair Non-termination in Multithreaded Programs. CAV 2012: 210-226 - [c82]Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi:
What's Decidable about Weak Memory Models? ESOP 2012: 26-46 - [c81]Ahmed Bouajjani, Michael Emmi:
Analysis of recursively parallel programs. POPL 2012: 203-214 - [c80]Ahmed Bouajjani, Michael Emmi:
Bounded Phase Analysis of Message-Passing Programs. TACAS 2012: 451-465 - [c79]Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu:
Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data. VMCAI 2012: 1-22 - 2011
- [c78]Mohamed Faouzi Atig, Ahmed Bouajjani, Gennaro Parlato:
Getting Rid of Store-Buffers in TSO Analysis. CAV 2011: 99-115 - [c77]Ahmed Bouajjani, Roland Meyer, Eike Möhlmann:
Deciding Robustness against Total Store Ordering. ICALP (2) 2011: 428-440 - [c76]Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu:
On inter-procedural analysis of programs with lists and data. PLDI 2011: 578-589 - [c75]Ahmed Bouajjani, Michael Emmi, Gennaro Parlato:
On Sequentializing Concurrent Programs. SAS 2011: 129-145 - 2010
- [c74]Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine, Mihaela Sighireanu:
Invariant Synthesis for Programs Manipulating Lists with Unbounded Data. CAV 2010: 72-88 - [c73]Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi:
On the verification problem for weak memory models. POPL 2010: 7-18 - 2009
- [c72]Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu:
A Logic-Based Framework for Reasoning about Composite Data Structures. CONCUR 2009: 178-195 - [c71]Ahmed Bouajjani, Cezara Dragoi, Yan Jurski, Mihaela Sighireanu:
Rewriting Systems over Nested Data Words. MEMICS 2009 - [c70]Mohamed Faouzi Atig, Ahmed Bouajjani:
On the Reachability Problem for Dynamic Networks of Concurrent Pushdown Systems. RP 2009: 1-2 - [c69]Mohamed Faouzi Atig, Ahmed Bouajjani, Shaz Qadeer:
Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads. TACAS 2009: 107-123 - 2008
- [c68]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 - [c67]Mohamed Faouzi Atig, Ahmed Bouajjani, Tayssir Touili:
On the Reachability Analysis of Acyclic Networks of Pushdown Systems. CONCUR 2008: 356-371 - [c66]Mohamed Faouzi Atig, Ahmed Bouajjani, Tayssir Touili:
Analyzing Asynchronous Programs with Preemption. FSTTCS 2008: 37-48 - [c65]Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar:
Computing Simulations over Tree Automata. TACAS 2008: 93-108 - [c64]Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Dejvuth Suwimonteerabuth:
SDSIrep: A Reputation System Based on SDSI. TACAS 2008: 501-516 - [c63]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 - [c62]Parosh Aziz Abdulla, Ahmed Bouajjani, Lukás Holík, Lisa Kaati, Tomás Vojnar:
Composed Bisimulation for Tree Automata. CIAA 2008: 212-222 - 2007
- [c61]Ahmed Bouajjani, Séverine Fratani, Shaz Qadeer:
Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures. CAV 2007: 207-220 - [c60]Ahmed Bouajjani, Peter Habermehl, Yan Jurski, Mihaela Sighireanu:
Rewriting Systems with Data. FCT 2007: 1-22 - [c59]Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu:
A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes. TACAS 2007: 690-705 - 2006
- [c58]Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomás Vojnar:
Programs with Lists Are Counter Automata. CAV 2006: 517-531 - [c57]Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani:
A Logic of Reachable Patterns in Linked Data-Structures. FoSSaCS 2006: 94-110 - [c56]Ahmed Bouajjani, Javier Esparza:
Rewriting Models of Boolean Programs. RTA 2006: 136-150 - [c55]Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, Tomás Vojnar:
Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. SAS 2006: 52-70 - [c54]Ahmed Bouajjani, Jan Strejcek, Tayssir Touili:
On Symbolic Verification of Weakly Extended PAD. EXPRESS 2006: 47-64 - 2005
- [c53]Ahmed Bouajjani, Markus Müller-Olm, Tayssir Touili:
Regular Symbolic Analysis of Dynamic Networks of Pushdown Systems. CONCUR 2005: 473-487 - [c52]Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejcek:
Reachability Analysis of Multithreaded Software with Asynchronous Communication. FSTTCS 2005: 348-359 - [c51]Ahmed Bouajjani, Tayssir Touili:
On Computing Reachability Sets of Process Rewrite Systems. RTA 2005: 484-499 - [c50]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 - [c49]Ahmed Bouajjani:
Regular Model Checking for Programs with Dynamic Memory. VISSAS 2005: 17-22 - [c48]Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, Tomás Vojnar:
Abstract Regular Tree Model Checking. INFINITY 2005: 37-48 - 2004
- [c47]Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar:
Abstract Regular Model Checking. CAV 2004: 372-386 - [c46]Ahmed Bouajjani, Antoine Meyer:
Symbolic Reachability Analysis of Higher-Order Context-Free Processes. FSTTCS 2004: 135-147 - [c45]Ahmed Bouajjani, Axel Legay, Pierre Wolper:
Handling Liveness Properties in (omega-)Regular Model Checking. INFINITY 2004: 101-115 - [c44]Ahmed Bouajjani, Javier Esparza, Tayssir Touili:
Reachability Analysis of Synchronized PA Systems. INFINITY 2004: 153-178 - 2003
- [c43]Ahmed Bouajjani, Peter Habermehl, Tomás Vojnar:
Verification of Parametric Concurrent Systems with Prioritized FIFO Resource Management. CONCUR 2003: 172-187 - [c42]Parosh Aziz Abdulla, Ahmed Bouajjani, Julien d'Orso:
Deciding Monotonic Games. CSL 2003: 1-14 - [c41]Ahmed Bouajjani:
Verification of Infinite State Systems (Tutorial). CSL 2003: 71 - [c40]Ahmed Bouajjani, Tayssir Touili:
Reachability Analysis of Process Rewrite Systems. FSTTCS 2003: 74-87 - [c39]Ahmed Bouajjani, Javier Esparza, Tayssir Touili:
A generic approach to the static analysis of concurrent programs with procedures. POPL 2003: 62-73 - 2002
- [c38]Ahmed Bouajjani, Tayssir Touili:
Extrapolating Tree Transformations. CAV 2002: 539-554 - [c37]Ahmed Bouajjani, Agathe Merceron:
Parametric Verification of a Group Membership Algorithm. FTRTFT 2002: 311-330 - 2001
- [c36]Aurore Annichini, Ahmed Bouajjani, Mihaela Sighireanu:
TReX: A Tool for Reachability Analysis of Complex Systems. CAV 2001: 368-372 - [c35]Ahmed Bouajjani:
Languages, Rewriting Systems, and Verification of Infinite-State Systems. ICALP 2001: 24-39 - [c34]Parosh Aziz Abdulla, Luc Boasson, Ahmed Bouajjani:
Effective Lossy Queue Languages. ICALP 2001: 639-651 - [c33]Eugene Asarin, Ahmed Bouajjani:
Perturbed Turing Machines and Hybrid Systems. LICS 2001: 269-278 - [c32]Ahmed Bouajjani, Anca Muscholl, Tayssir Touili:
Permutation Rewriting and Algorithmic Verification. LICS 2001: 399-408 - [c31]Ahmed Bouajjani, Peter Habermehl, Richard Mayr:
Automatic Verification of Recursive Procedures with One Integer Parameter. MFCS 2001: 198-211 - [c30]Ahmed Bouajjani, Aurore Collomb-Annichini, Yassine Lakhnech, Mihaela Sighireanu:
Analyzing Fair Parametric Extended Automata. SAS 2001: 335-355 - 2000
- [c29]Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, Tayssir Touili:
Regular Model Checking. CAV 2000: 403-418 - [c28]Aurore Annichini, Eugene Asarin, Ahmed Bouajjani:
Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. CAV 2000: 419-434 - 1999
- [c27]Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson:
Handling Global Conditions in Parameterized System Verification. CAV 1999: 134-145 - [c26]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 - [c25]Ahmed Bouajjani, Richard Mayr:
Model Checking Lossy Vector Addition Systems. STACS 1999: 323-333 - [c24]Parosh Aziz Abdulla, Aurore Annichini, Ahmed Bouajjani:
Symbolic Verification of Lossy Channel Systems: Application to the Bounded Retransmission Protocol. TACAS 1999: 208-222 - 1998
- [c23]Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson:
On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels. CAV 1998: 305-318 - 1997
- [c22]Ahmed Bouajjani, Javier Esparza, Oded Maler:
Reachability Analysis of Pushdown Automata: Application to Model-Checking. CONCUR 1997: 135-150 - [c21]Ahmed Bouajjani, Peter Habermehl:
Symbolic Reachability Analysis of FIFO Channel Systems with Nonregular Sets of Configurations (Extended Abstract). ICALP 1997: 560-570 - [c20]Ahmed Bouajjani, Stavros Tripakis, Sergio Yovine:
On-the-fly symbolic model checking for real-time systems. RTSS 1997: 25-34 - 1996
- [c19]Ahmed Bouajjani, Peter Habermehl:
Constrained Properties, Semilinear Systems, and Petri Nets. CONCUR 1996: 481-497 - [c18]Ahmed Bouajjani, Yassine Lakhnech, Sergio Yovine:
Model-Checking for Extended Timed Temporal Logics. FTRTFT 1996: 306-326 - 1995
- [c17]Ahmed Bouajjani, Yassine Lakhnech, Riadh Robbana:
From Duration Calculus To Linear Hybrid Automata. CAV 1995: 196-210 - [c16]Ahmed Bouajjani, Riadh Robbana:
Verifying omega-Regular Properties for a Subclass of Linear Hybrid Systems. CAV 1995: 437-450 - [c15]Ahmed Bouajjani, Yassine Lakhnech:
Temporal Logic + Timed Automata: Expressiveness and Decidability. CONCUR 1995: 531-545 - [c14]Ahmed Bouajjani, Yassine Lakhnech:
Logics vs. Automata: The Hybrid Case. Hybrid Systems 1995: 531-542 - [c13]Ahmed Bouajjani, Rachid Echahed, Peter Habermehl:
On the Verification Problem of Nonregular Properties for Nonregular Processes. LICS 1995: 123-133 - [c12]Ahmed Bouajjani, Rachid Echahed, Peter Habermehl:
Verifying Infinite State Processes with Sequential and Parallel Composition. POPL 1995: 95-106 - 1994
- [c11]Ahmed Bouajjani, Rachid Echahed, Riadh Robbana:
Verification of Context-Free Timed Systems Using Linear Hybrid Observers. CAV 1994: 118-131 - [c10]Ahmed Bouajjani, Rachid Echahed, Riadh Robbana:
Verification of Nonregular Temporal Properties for Context-Free Processes. CONCUR 1994: 81-97 - [c9]Ahmed Bouajjani, Rachid Echahed, Riadh Robbana:
Verfying Invariance Properties of Timed Systems with Duration Variables. FTRTFT 1994: 193-210 - [c8]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 - 1993
- [c7]Ahmed Bouajjani, Rachid Echahed, Joseph Sifakis:
On Model Checking for Real-Time Properties with Durations. LICS 1993: 147-159 - 1992
- [c6]Saddek Bensalem, Ahmed Bouajjani, Claire Loiseaux, Joseph Sifakis:
Property Preserving Simulations. CAV 1992: 260-273 - 1991
- [c5]Ahmed Bouajjani, Jean-Claude Fernandez, Susanne Graf, Carlos Rodriguez, Joseph Sifakis:
Safety for Branching Time Semantics. ICALP 1991: 76-92 - [c4]Ahmed Bouajjani, Joseph Sifakis:
Verification for Finite Systems (Extended Abstract). TAPSOFT, Vol.2 1991: 55-57 - 1990
- [c3]Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs:
Minimal Model Generation. CAV 1990: 197-203 - [c2]Ahmed Bouajjani, Jean-Claude Fernandez, Nicolas Halbwachs:
Minimal Model Generation. CAV (DIMACS/AMS volume) 1990: 85-92 - 1988
- [c1]Ahmed Bouajjani, Susanne Graf, Joseph Sifakis:
A logig for the description of behaviours and properties of concurrent systems. REX Workshop 1988: 398-410
Parts in Books or Collections
- 2018
- [p1]Rajeev Alur, Ahmed Bouajjani, Javier Esparza:
Model Checking Procedural Programs. Handbook of Model Checking 2018: 541-572
Editorship
- 2022
- [e7]Ahmed Bouajjani, Lukás Holík, Zhilin Wu:
Automated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings. Lecture Notes in Computer Science 13505, Springer 2022, ISBN 978-3-031-19991-2 [contents] - 2017
- [e6]Ahmed Bouajjani, Alexandra Silva:
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. Lecture Notes in Computer Science 10321, Springer 2017, ISBN 978-3-319-60224-0 [contents] - [e5]Ahmed Bouajjani, David Monniaux:
Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings. Lecture Notes in Computer Science 10145, Springer 2017, ISBN 978-3-319-52233-3 [contents] - 2015
- [e4]Ahmed Bouajjani, Hugues Fauconnier:
Networked Systems - Third International Conference, NETYS 2015, Agadir, Morocco, May 13-15, 2015, Revised Selected Papers. Lecture Notes in Computer Science 9466, Springer 2015, ISBN 978-3-319-26849-1 [contents] - 2010
- [e3]Ahmed Bouajjani, Wei-Ngan Chin:
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 [contents] - 2009
- [e2]Ahmed Bouajjani, Oded Maler:
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 [contents] - 2006
- [e1]Parosh Aziz Abdulla, Ahmed Bouajjani, Markus Müller-Olm:
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 [contents]
Informal and Other Publications
- 2023
- [i26]Ahmed Bouajjani, Constantin Enea, Enrique Román-Calvo:
Dynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation Levels. CoRR abs/2303.12606 (2023) - 2022
- [i25]Ahmed Bouajjani, Wael-Amine Boutglay, Peter Habermehl:
Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes. CoRR abs/2205.14943 (2022) - [i24]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri:
Automated Synthesis of Asynchronizations. CoRR abs/2209.06648 (2022) - 2021
- [i23]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea:
Checking Robustness Between Weak Transactional Consistency Models. CoRR abs/2101.09032 (2021) - 2020
- [i22]Rachid Zennou, Ranadeep Biswas, Ahmed Bouajjani, Constantin Enea, Mohammed Erradi:
Checking Causal Consistency of Distributed Databases. CoRR abs/2011.09753 (2020) - 2019
- [i21]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea:
Checking Robustness Against Snapshot Isolation. CoRR abs/1905.08406 (2019) - [i20]Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea:
Robustness Against Transactional Causal Consistency. CoRR abs/1906.12095 (2019) - 2018
- [i19]Ahmed Bouajjani, Constantin Enea, Suha Orhun Mutluergil, Serdar Tasiran:
Reasoning About TSO Programs Using Reduction and Abstraction. CoRR abs/1804.05196 (2018) - [i18]Ahmed Bouajjani, Constantin Enea, Kailiang Ji, Shaz Qadeer:
On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony. CoRR abs/1804.06612 (2018) - 2017
- [i17]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo:
The Benefits of Duality in Verifying Concurrent Programs under TSO. CoRR abs/1701.08682 (2017) - [i16]Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo:
Context-Bounded Analysis for POWER. CoRR abs/1702.01655 (2017) - [i15]Ahmed Bouajjani, Michael Emmi, Constantin Enea, Suha Orhun Mutluergil:
Proving linearizability using forward simulations. CoRR abs/1702.02705 (2017) - [i14]Ahmed Bouajjani, Constantin Enea, Chao Wang:
Checking Linearizability of Concurrent Priority Queues. CoRR abs/1707.00639 (2017) - 2016
- [i13]Ahmed Bouajjani, Constantin Enea, Rachid Guerraoui, Jad Hamza:
On Verifying Causal Consistency. CoRR abs/1611.00580 (2016) - 2015
- [i12]Ahmed Bouajjani, Georgel Calin, Egor Derevenetc, Roland Meyer:
Lazy TSO Reachability. CoRR abs/1501.02683 (2015) - [i11]Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza:
On Reducing Linearizability to State Reachability. CoRR abs/1502.06882 (2015) - 2012
- [i10]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) - [i9]Ahmed Bouajjani, Egor Derevenetc, Roland Meyer:
Robustness Checking against TSO: Attacks and Defence. CoRR abs/1208.6152 (2012) - 2009
- [i8]Ahmed Bouajjani, Axel Legay, Pierre Wolper:
A Framework to Handle Linear Temporal Properties in (\omega-)Regular Model Checking. CoRR abs/0901.4080 (2009) - 2008
- [i7]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 - 2007
- [i6]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) - [i5]Ahmed Bouajjani, Antoine Meyer:
Symbolic Reachability Analysis of Higher-Order Context-Free Processes. CoRR abs/0705.3888 (2007) - 2006
- [i4]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 - [i3]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 - [i2]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 - 2005
- [i1]Ahmed Bouajjani, Agathe Merceron:
Parametric Verification of a Group Membership Algorithm. CoRR abs/cs/0505033 (2005)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:21 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
