Edit Profile (opens in new tab) Bouajjani, Ahmed Co-Author Distance Author ID: bouajjani.ahmed Published as: Bouajjani, Ahmed; Bouajjani, A. Documents Indexed: 106 Publications since 1989 7 Contributions as Editor Software Indexed: 1 Package Co-Authors: 88 Co-Authors with 111 Joint Publications 1,687 Co-Co-Authors all top 5 Co-Authors 2 single-authored 26 Enea, Constantin 17 Habermehl, Peter 14 Atig, Mohamed Faouzi 13 Touili, Tayssir 12 Abdulla, Parosh Aziz 12 Vojnar, Tomáš 9 Sighireanu, Mihaela 8 Emmi, Michael 8 Esparza, Javier 6 Hamza, Jad 5 Beillahi, Sidi Mohamed 5 Dragoi, Cezara 5 Holík, Lukáš 4 Fernandez, Jean-Claude 4 Jurski, Yan 4 Maler, Oded 4 Qadeer, Shaz 4 Saivasan, Prakash 3 Annichini, Aurore 3 Erradi, Mohammed 3 Graf, Susanne 3 Halbwachs, Nicolas 3 Jonsson, Bengt 3 Kaati, Lisa 3 Lahiri, Shuvendu Kumar 3 Mayr, Richard M. 3 Meyer, Antoine 3 Moro, Pierre 3 Zennou, Rachid 2 Bensalem, Saddek 2 Biswas, Ranadeep 2 Bozga, Marius 2 Burckhardt, Sebastian 2 Collomb-Annichini, Aurore 2 d’Orso, Julien 2 Iosif, Radu 2 Kumar, K. Narayan 2 Lakhnech, Yassine 2 Merceron, Agathe 2 Meyer, Roland 2 Musuvathi, Madanlal 2 Mutluergil, Suha Orhun 2 Narayan, Kumar K. 2 Ngo, Tuan Phong 2 Nilsson, Marcus 2 Rabinovich, Alexander 2 Rogalewicz, Adam 2 Sagiv, Mooly 2 Sifakis, Joseph 2 Strejček, Jan 2 Tasiran, Serdar 2 Wolper, Pierre 2 Yorsh, Greta 1 Alur, Rajeev 1 Asarin, Eugene 1 Boasson, Luc 1 Boutglay, Wael-Amine 1 Cederberg, Jonathan 1 Chin, Wei-Ngan 1 Derevenetc, Egor 1 Fauconnier, Hugues 1 Finkel, Alain 1 Fratani, Séverine 1 Guerraoui, Rachid 1 Haziza, Frédéric 1 Ji, Kailiang 1 Legay, Axel 1 Loiseaux, Claire 1 Möhlmann, Eike 1 Monniaux, David P. 1 Mukund, Madhavan 1 Müller-Olm, Markus 1 Muscholl, Anca 1 Ozkan, Burcu Kulahcioglu 1 Parlato, Gennaro 1 Ratel, Christophe 1 Rezine, Ahmed 1 Rossmanith, Peter 1 Schwoon, Stefan 1 Shenoy R., Gautham 1 Sifkis, J. 1 Silva, Alexandra 1 Suresh, S. P. 1 Tripakis, Stavros 1 Wang, Chao 1 Willems, Bernard 1 Wu, Zhilin 1 Yovine, Sergio all top 5 Serials 7 Formal Methods in System Design 5 Lecture Notes in Computer Science 4 Logical Methods in Computer Science 2 Computing 2 Theoretical Computer Science 2 Information and Computation 2 International Journal of Foundations of Computer Science 1 Information Processing Letters 1 Science of Computer Programming 1 Journal of Logic and Computation 1 The Journal of Logic and Algebraic Programming 1 Theory and Practice of Logic Programming Fields 113 Computer science (68-XX) 11 Mathematical logic and foundations (03-XX) 7 General and overarching topics; collections (00-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 93 Publications have been cited 1,044 times in 658 Documents Cited by ▼ Year ▼ Reachability analysis of pushdown automata: application to model-checking. Zbl 1512.68135 Bouajjani, Ahmed; Esparza, Javier; Maler, Oded 102 1997 Property preserving abstractions for the verification of concurrent systems. Zbl 0829.68053 Loiseaux, C.; Graf, S.; Sifakis, J.; Bouajjani, A.; Bensalem, S. 44 1995 Regular model checking. Zbl 0974.68118 Bouajjani, Ahmed; Jonsson, Bengt; Nilsson, Marcus; Touili, Tayssir 44 2000 Using forward reachability analysis for verification of lossy channel systems. Zbl 1073.68675 Abdulla, Parosh Aziz; Collomb-Annichini, Aurore; Bouajjani, Ahmed; Jonsson, Bengt 33 2004 Abstract regular model checking. Zbl 1103.68071 Bouajjani, Ahmed; Habermehl, Peter; Vojnar, Tomáš 28 2004 Programs with lists are counter automata. Zbl 1188.68181 Bouajjani, Ahmed; Bozga, Marius; Habermehl, Peter; Iosif, Radu; Moro, Pierre; Vojnar, Tomáš 24 2006 Regular symbolic analysis of dynamic networks of pushdown systems. Zbl 1134.68427 Bouajjani, Ahmed; Müller-Olm, Markus; Touili, Tayssir 24 2005 A generic approach to the static analysis of concurrent programs with procedures. Zbl 1321.68185 Bouajjani, Ahmed; Esparza, Javier; Touili, Tayssir 23 2003 Abstract regular tree model checking of complex dynamic data structures. Zbl 1225.68067 Bouajjani, Ahmed; Habermehl, Peter; Rogalewicz, Adam; Vojnar, Tomáš 23 2006 On the verification problem for weak memory models. Zbl 1312.68050 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Burckhardt, Sebastian; Musuvathi, Madanlal 22 2010 Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Zbl 0933.68089 Bouajjani, Ahmed; Habermehl, Peter 21 1999 Checking timed Büchi automata emptiness efficiently. Zbl 1085.68083 Tripakis, Stavros; Yovine, Sergio; Bouajjani, Ahmed 21 2005 Safety for branching time semantics. Zbl 0769.68089 Bouajjani, A.; Fernandez, J. C.; Graf, S.; Rodriguez, C.; Sifakis, J. 20 1991 Permutation rewriting and algorithmic verification. Zbl 1107.68052 Bouajjani, Ahmed; Muscholl, Anca; Touili, Tayssir 19 2007 Abstract regular tree model checking. Zbl 1273.68221 Bouajjani, Ahmed; Habermehl, Peter; Rogalewicz, Adam; Vojnar, Tomáš 18 2006 Handling global conditions in parameterized system verification. Zbl 1046.68573 Abdulla, Parosh Aziz; Bouajjani, Ahmed; Jonsson, Bengt; Nilsson, Marcus 17 1999 On the completeness of verifying message passing programs under bounded asynchrony. Zbl 1511.68073 Bouajjani, Ahmed; Enea, Constantin; Ji, Kailiang; Qadeer, Shaz 17 2018 Context-bounded analysis for concurrent programs with dynamic creation of threads. Zbl 1237.68056 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Qadeer, Shaz 16 2011 Verifying concurrent programs against sequential specifications. Zbl 1381.68048 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Hamza, Jad 16 2013 Reachability analysis of multithreaded software with asynchronous communication. Zbl 1172.68422 Bouajjani, Ahmed; Esparza, Javier; Schwoon, Stefan; Strejček, Jan 16 2005 TREX: A tool for reachability analysis of complex systems. Zbl 0991.68645 Annichini, Aurore; Bouajjani, Ahmed; Sighireanu, Mihaela 16 2001 Checking and enforcing robustness against TSO. Zbl 1381.68039 Bouajjani, Ahmed; Derevenetc, Egor; Meyer, Roland 15 2013 On the reachability analysis of acyclic networks of pushdown systems. Zbl 1160.68451 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Touili, Tayssir 15 2008 A logic of reachable patterns in linked data-structures. Zbl 1180.68131 Yorsh, Greta; Rabinovich, Alexander; Sagiv, Mooly; Meyer, Antoine; Bouajjani, Ahmed 14 2006 Minimal model generation. Zbl 0765.68114 Bouajjani, A.; Fernandez, J.-C.; Halbwachs, N. 13 1991 Reachability analysis of process rewrite systems. Zbl 1205.68183 Bouajjani, Ahmed; Touili, Tayssir 13 2003 Constrained properties, semilinear systems, and Petri nets. Zbl 1514.68125 Bouajjani, Ahmed; Habermehl, Peter 13 1996 Verifying programs with dynamic 1-selector-linked structures in regular model checking. Zbl 1087.68585 Bouajjani, Ahmed; Habermehl, Peter; Moro, Pierre; Vojnar, Tomáš 12 2005 On computing reachability sets of process rewrite systems. Zbl 1078.68652 Bouajjani, Ahmed; Touili, Tayssir 12 2005 Model checking procedural programs. Zbl 1392.68226 Alur, Rajeev; Bouajjani, Ahmed; Esparza, Javier 12 2018 Model checking lossy vector addition systems. Zbl 0926.03035 Bouajjani, Ahmed; Mayr, Richard 12 1999 Deciding monotonic games. Zbl 1116.68491 Abdulla, Parosh Aziz; Bouajjani, Ahmed; d’Orso, Julien 12 2003 Tractable refinement checking for concurrent objects. Zbl 1345.68096 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Hamza, Jad 12 2015 A generic approach to the static analysis of concurrent programs with procedures. Zbl 1101.68457 Bouajjani, Ahmed; Esparza, Javier; Touili, Tayssir 11 2003 Computing simulations over tree automata. Efficient techniques for reducing tree automata. Zbl 1134.68391 Abdulla, Parosh A.; Bouajjani, Ahmed; Holík, Lukáš; Kaati, Lisa; Vojnar, Tomáš 11 2008 On verifying causal consistency. Zbl 1380.68270 Bouajjani, Ahmed; Enea, Constantin; Guerraoui, Rachid; Hamza, Jad 11 2017 Context-bounded analysis for concurrent programs with dynamic creation of threads. Zbl 1234.68068 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Qadeer, Shaz 11 2009 Antichain-based universality and inclusion testing over nondeterministic finite tree automata. Zbl 1172.68493 Bouajjani, Ahmed; Habermehl, Peter; Holík, Lukáš; Touili, Tayssir; Vojnar, Tomáš 11 2008 A logic-based framework for reasoning about composite data structures. Zbl 1254.68146 Bouajjani, Ahmed; Drăgoi, Cezara; Enea, Constantin; Sighireanu, Mihaela 10 2009 On reducing linearizability to state reachability. Zbl 1395.68089 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Hamza, Jad 10 2015 Symbolic techniques for parametric reasoning about counter and clock systems. Zbl 0974.68523 Annichini, Aurore; Asarin, Eugene; Bouajjani, Ahmed 10 2000 Extrapolating tree transformations. Zbl 1010.68085 Bouajjani, Ahmed; Touili, Tayssir 10 2002 What’s decidable about weak memory models? Zbl 1352.68056 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Burckhardt, Sebastian; Musuvathi, Madanlal 10 2012 Monotonic abstraction for programs with dynamic memory heaps. Zbl 1155.68423 Abdulla, Parosh Aziz; Bouajjani, Ahmed; Cederberg, Jonathan; Haziza, Frédéric; Rezine, Ahmed 9 2008 Programs with lists are counter automata. Zbl 1217.68059 Bouajjani, Ahmed; Bozga, Marius; Habermehl, Peter; Iosif, Radu; Moro, Pierre; Vojnar, Tomáš 9 2011 Rewriting systems with data. Zbl 1135.68467 Bouajjani, Ahmed; Habermehl, Peter; Jurski, Yan; Sighireanu, Mihaela 9 2007 Analysis of recursively parallel programs. Zbl 1321.68184 Bouajjani, Ahmed; Emmi, Michael 8 2012 Deciding robustness against total store ordering. Zbl 1333.68082 Bouajjani, Ahmed; Meyer, Roland; Möhlmann, Eike 7 2011 Verifying eventual consistency of optimistic replication systems. Zbl 1284.68383 Bouajjani, Ahmed; Enea, Constantin; Hamza, Jad 7 2014 Automatic verification of recursive procedures with one integer parameter. Zbl 1053.68060 Bouajjani, Ahmed; Habermehl, Peter; Mayr, Richard 7 2003 Context-bounded analysis of multithreaded programs with dynamic linked structures. Zbl 1135.68365 Bouajjani, Ahmed; Fratani, Séverine; Qadeer, Shaz 7 2007 A load-buffer semantics for total store ordering. Zbl 1459.68038 Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Ngo, Tuan Phong 7 2018 Analyzing asynchronous programs with preemption. Zbl 1248.68348 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Touili, Tayssir 7 2008 On bounded reachability analysis of shared memory systems. Zbl 1360.68624 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Kumar, K. Narayan; Saivasan, Prakash 7 2014 Monotonic and downward closed games. Zbl 1133.68042 Abdulla, Parosh Aziz; Bouajjani, Ahmed; D’Orso, Julien 6 2008 Linear-time model-checking for multithreaded programs under scope-bounding. Zbl 1375.68076 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Narayan Kumar, K.; Saivasan, Prakash 6 2012 Accurate invariant checking for programs manipulating lists and arrays with infinite data. Zbl 1374.68112 Bouajjani, Ahmed; Drăgoi, Cezara; Enea, Constantin; Sighireanu, Mihaela 6 2012 Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Zbl 1401.68186 Bouajjani, Ahmed; Habermehl, Peter 6 1997 A logic of reachable patterns in linked data-structures. Zbl 1121.03040 Yorsh, Greta; Rabinovich, Alexander; Sagiv, Mooly; Meyer, Antoine; Bouajjani, Ahmed 6 2007 Languages, rewriting systems, and verification of infinite-state systems. Zbl 0986.68517 Bouajjani, Ahmed 6 2001 Effective lossy queue languages. Zbl 0986.68044 Aziz Abdulla, Parosh; Boasson, Luc; Bouajjani, Ahmed 6 2001 Bounded phase analysis of message-passing programs. Zbl 1352.68057 Bouajjani, Ahmed; Emmi, Michael 6 2012 Verification of parametric concurrent systems with prioritised FIFO resource management. Zbl 1138.68464 Bouajjani, Ahmed; Habermehl, Peter; Vojnar, Tomáš 5 2008 Robustness against transactional causal consistency. Zbl 1509.68157 Beillahi, Sidi Mohamed; Bouajjani, Ahmed; Enea, Constantin 5 2021 Handling liveness properties in (\(\omega\)-)regular model checking. Zbl 1272.68227 Bouajjani, Ahmed; Legay, Axel; Wolper, Pierre 5 2005 Computer aided verification. 21st international conference, CAV 2009, Grenoble, France, June 26–July 2, 2009. Proceedings. Zbl 1165.68004 4 2009 Reachability analysis of synchronized PA systems. Zbl 1272.68290 Bouajjani, Ahmed; Esparza, Javier; Touili, Tayssir 4 2005 Rewriting models of Boolean programs. Zbl 1151.68440 Bouajjani, Ahmed; Esparza, Javier 4 2006 Symbolic reachability analysis of higher-order context-free processes. Zbl 1117.68395 Bouajjani, Ahmed; Meyer, Antoine 4 2004 The benefits of duality in verifying concurrent programs under TSO. Zbl 1392.68142 Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Ngo, Tuan Phong 4 2016 Abstract domains for automated reasoning about list-manipulating programs with infinite data. Zbl 1325.68058 Bouajjani, Ahmed; Drăgoi, Cezara; Enea, Constantin; Sighireanu, Mihaela 4 2012 Minimal state graph generation. Zbl 0769.68090 Bouajjani, A.; Fernandez, J.-C.; Halbwachs, N.; Raymond, P.; Ratel, C. 3 1992 Composed bisimulation for tree automata. Zbl 1172.68487 Abdulla, Parosh A.; Bouajjani, Ahmed; Holík, Lukáš; Kaati, Lisa; Vojnar, Tomáš 3 2008 Context-bounded analysis of TSO systems. Zbl 1416.68050 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Parlato, Gennaro 3 2014 Proving linearizability using forward simulations. Zbl 1494.68067 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Mutluergil, Suha Orhun 3 2017 Abstract semantic diffing of evolving concurrent programs. Zbl 1420.68051 Bouajjani, Ahmed; Enea, Constantin; Lahiri, Shuvendu K. 3 2017 An efficient automata approach to some problems on context-free grammars. Zbl 1137.68418 Bouajjani, Ahmed; Esparza, Javier; Finkel, Alain; Maler, Oded; Rossmanith, Peter; Willems, Bernard; Wolper, Pierre 2 2000 On reducing linearizability to state reachability. Zbl 1395.68090 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Hamza, Jad 2 2018 Checking robustness between weak transactional consistency models. Zbl 1473.68063 Beillahi, Sidi Mohamed; Bouajjani, Ahmed; Enea, Constantin 2 2021 Checking robustness against snapshot isolation. Zbl 1533.68142 Beillahi, Sidi Mohamed; Bouajjani, Ahmed; Enea, Constantin 2 2019 Robustness against transactional causal consistency. Zbl 07649938 Beillahi, Sidi Mohamed; Bouajjani, Ahmed; Enea, Constantin 2 2019 Verifying robustness of event-driven asynchronous programs against concurrency. Zbl 1485.68054 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Ozkan, Burcu Kulahcioglu; Tasiran, Serdar 2 2017 Minimal model generation. Zbl 0786.68056 Bouajjani, A.; Fernandez, J.-C.; Halbwachs, N. 1 1991 Composed bisimulation for tree automata. Zbl 1176.68098 Abdulla, Parosh Aziz; Bouajjani, Ahmed; Holík, Lukáš; Kaati, Lisa; Vojnar, Tomáš 1 2009 Automatic verification of recursive procedures with one integer parameter. Zbl 1005.68096 Bouajjani, Ahmed; Habermehl, Peter; Mayr, Richard 1 2001 Parametric verification of a group membership algorithm. Zbl 1278.68159 Bouajjani, Ahmed; Merceron, Agathe 1 2002 Checking linearizability of concurrent priority queues. Zbl 1442.68126 Bouajjani, Ahmed; Enea, Constantin; Wang, Chao 1 2017 Formalizing and checking multilevel consistency. Zbl 1544.68087 Bouajjani, Ahmed; Enea, Constantin; Mukund, Madhavan; Shenoy R., Gautham; Suresh, S. P. 1 2020 A logic for the description of behaviors and properties of concurrent systems. (Technical contribution). Zbl 0683.68012 Bouajjani, A.; Graf, S.; Sifkis, J. 1 1989 Gradual consistency checking. Zbl 1533.68182 Zennou, Rachid; Bouajjani, Ahmed; Enea, Constantin; Erradi, Mohammed 1 2019 Data-driven numerical invariant synthesis with automatic generation of attributes. Zbl 1514.68124 Bouajjani, Ahmed; Boutglay, Wael-Amine; Habermehl, Peter 1 2022 Boosting sequential consistency checking using saturation. Zbl 1517.68086 Zennou, Rachid; Atig, Mohamed Faouzi; Biswas, Ranadeep; Bouajjani, Ahmed; Enea, Constantin; Erradi, Mohammed 1 2020 Verification of asynchronous programs with nested locks. Zbl 1491.68105 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Narayan, Kumar K.; Saivasan, Prakash 1 2018 Data-driven numerical invariant synthesis with automatic generation of attributes. Zbl 1514.68124 Bouajjani, Ahmed; Boutglay, Wael-Amine; Habermehl, Peter 1 2022 Robustness against transactional causal consistency. Zbl 1509.68157 Beillahi, Sidi Mohamed; Bouajjani, Ahmed; Enea, Constantin 5 2021 Checking robustness between weak transactional consistency models. Zbl 1473.68063 Beillahi, Sidi Mohamed; Bouajjani, Ahmed; Enea, Constantin 2 2021 Formalizing and checking multilevel consistency. Zbl 1544.68087 Bouajjani, Ahmed; Enea, Constantin; Mukund, Madhavan; Shenoy R., Gautham; Suresh, S. P. 1 2020 Boosting sequential consistency checking using saturation. Zbl 1517.68086 Zennou, Rachid; Atig, Mohamed Faouzi; Biswas, Ranadeep; Bouajjani, Ahmed; Enea, Constantin; Erradi, Mohammed 1 2020 Checking robustness against snapshot isolation. Zbl 1533.68142 Beillahi, Sidi Mohamed; Bouajjani, Ahmed; Enea, Constantin 2 2019 Robustness against transactional causal consistency. Zbl 07649938 Beillahi, Sidi Mohamed; Bouajjani, Ahmed; Enea, Constantin 2 2019 Gradual consistency checking. Zbl 1533.68182 Zennou, Rachid; Bouajjani, Ahmed; Enea, Constantin; Erradi, Mohammed 1 2019 On the completeness of verifying message passing programs under bounded asynchrony. Zbl 1511.68073 Bouajjani, Ahmed; Enea, Constantin; Ji, Kailiang; Qadeer, Shaz 17 2018 Model checking procedural programs. Zbl 1392.68226 Alur, Rajeev; Bouajjani, Ahmed; Esparza, Javier 12 2018 A load-buffer semantics for total store ordering. Zbl 1459.68038 Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Ngo, Tuan Phong 7 2018 On reducing linearizability to state reachability. Zbl 1395.68090 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Hamza, Jad 2 2018 Verification of asynchronous programs with nested locks. Zbl 1491.68105 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Narayan, Kumar K.; Saivasan, Prakash 1 2018 On verifying causal consistency. Zbl 1380.68270 Bouajjani, Ahmed; Enea, Constantin; Guerraoui, Rachid; Hamza, Jad 11 2017 Proving linearizability using forward simulations. Zbl 1494.68067 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Mutluergil, Suha Orhun 3 2017 Abstract semantic diffing of evolving concurrent programs. Zbl 1420.68051 Bouajjani, Ahmed; Enea, Constantin; Lahiri, Shuvendu K. 3 2017 Verifying robustness of event-driven asynchronous programs against concurrency. Zbl 1485.68054 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Ozkan, Burcu Kulahcioglu; Tasiran, Serdar 2 2017 Checking linearizability of concurrent priority queues. Zbl 1442.68126 Bouajjani, Ahmed; Enea, Constantin; Wang, Chao 1 2017 The benefits of duality in verifying concurrent programs under TSO. Zbl 1392.68142 Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Bouajjani, Ahmed; Ngo, Tuan Phong 4 2016 Tractable refinement checking for concurrent objects. Zbl 1345.68096 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Hamza, Jad 12 2015 On reducing linearizability to state reachability. Zbl 1395.68089 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Hamza, Jad 10 2015 Verifying eventual consistency of optimistic replication systems. Zbl 1284.68383 Bouajjani, Ahmed; Enea, Constantin; Hamza, Jad 7 2014 On bounded reachability analysis of shared memory systems. Zbl 1360.68624 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Kumar, K. Narayan; Saivasan, Prakash 7 2014 Context-bounded analysis of TSO systems. Zbl 1416.68050 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Parlato, Gennaro 3 2014 Verifying concurrent programs against sequential specifications. Zbl 1381.68048 Bouajjani, Ahmed; Emmi, Michael; Enea, Constantin; Hamza, Jad 16 2013 Checking and enforcing robustness against TSO. Zbl 1381.68039 Bouajjani, Ahmed; Derevenetc, Egor; Meyer, Roland 15 2013 What’s decidable about weak memory models? Zbl 1352.68056 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Burckhardt, Sebastian; Musuvathi, Madanlal 10 2012 Analysis of recursively parallel programs. Zbl 1321.68184 Bouajjani, Ahmed; Emmi, Michael 8 2012 Linear-time model-checking for multithreaded programs under scope-bounding. Zbl 1375.68076 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Narayan Kumar, K.; Saivasan, Prakash 6 2012 Accurate invariant checking for programs manipulating lists and arrays with infinite data. Zbl 1374.68112 Bouajjani, Ahmed; Drăgoi, Cezara; Enea, Constantin; Sighireanu, Mihaela 6 2012 Bounded phase analysis of message-passing programs. Zbl 1352.68057 Bouajjani, Ahmed; Emmi, Michael 6 2012 Abstract domains for automated reasoning about list-manipulating programs with infinite data. Zbl 1325.68058 Bouajjani, Ahmed; Drăgoi, Cezara; Enea, Constantin; Sighireanu, Mihaela 4 2012 Context-bounded analysis for concurrent programs with dynamic creation of threads. Zbl 1237.68056 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Qadeer, Shaz 16 2011 Programs with lists are counter automata. Zbl 1217.68059 Bouajjani, Ahmed; Bozga, Marius; Habermehl, Peter; Iosif, Radu; Moro, Pierre; Vojnar, Tomáš 9 2011 Deciding robustness against total store ordering. Zbl 1333.68082 Bouajjani, Ahmed; Meyer, Roland; Möhlmann, Eike 7 2011 On the verification problem for weak memory models. Zbl 1312.68050 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Burckhardt, Sebastian; Musuvathi, Madanlal 22 2010 Context-bounded analysis for concurrent programs with dynamic creation of threads. Zbl 1234.68068 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Qadeer, Shaz 11 2009 A logic-based framework for reasoning about composite data structures. Zbl 1254.68146 Bouajjani, Ahmed; Drăgoi, Cezara; Enea, Constantin; Sighireanu, Mihaela 10 2009 Computer aided verification. 21st international conference, CAV 2009, Grenoble, France, June 26–July 2, 2009. Proceedings. Zbl 1165.68004 4 2009 Composed bisimulation for tree automata. Zbl 1176.68098 Abdulla, Parosh Aziz; Bouajjani, Ahmed; Holík, Lukáš; Kaati, Lisa; Vojnar, Tomáš 1 2009 On the reachability analysis of acyclic networks of pushdown systems. Zbl 1160.68451 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Touili, Tayssir 15 2008 Computing simulations over tree automata. Efficient techniques for reducing tree automata. Zbl 1134.68391 Abdulla, Parosh A.; Bouajjani, Ahmed; Holík, Lukáš; Kaati, Lisa; Vojnar, Tomáš 11 2008 Antichain-based universality and inclusion testing over nondeterministic finite tree automata. Zbl 1172.68493 Bouajjani, Ahmed; Habermehl, Peter; Holík, Lukáš; Touili, Tayssir; Vojnar, Tomáš 11 2008 Monotonic abstraction for programs with dynamic memory heaps. Zbl 1155.68423 Abdulla, Parosh Aziz; Bouajjani, Ahmed; Cederberg, Jonathan; Haziza, Frédéric; Rezine, Ahmed 9 2008 Analyzing asynchronous programs with preemption. Zbl 1248.68348 Atig, Mohamed Faouzi; Bouajjani, Ahmed; Touili, Tayssir 7 2008 Monotonic and downward closed games. Zbl 1133.68042 Abdulla, Parosh Aziz; Bouajjani, Ahmed; D’Orso, Julien 6 2008 Verification of parametric concurrent systems with prioritised FIFO resource management. Zbl 1138.68464 Bouajjani, Ahmed; Habermehl, Peter; Vojnar, Tomáš 5 2008 Composed bisimulation for tree automata. Zbl 1172.68487 Abdulla, Parosh A.; Bouajjani, Ahmed; Holík, Lukáš; Kaati, Lisa; Vojnar, Tomáš 3 2008 Permutation rewriting and algorithmic verification. Zbl 1107.68052 Bouajjani, Ahmed; Muscholl, Anca; Touili, Tayssir 19 2007 Rewriting systems with data. Zbl 1135.68467 Bouajjani, Ahmed; Habermehl, Peter; Jurski, Yan; Sighireanu, Mihaela 9 2007 Context-bounded analysis of multithreaded programs with dynamic linked structures. Zbl 1135.68365 Bouajjani, Ahmed; Fratani, Séverine; Qadeer, Shaz 7 2007 A logic of reachable patterns in linked data-structures. Zbl 1121.03040 Yorsh, Greta; Rabinovich, Alexander; Sagiv, Mooly; Meyer, Antoine; Bouajjani, Ahmed 6 2007 Programs with lists are counter automata. Zbl 1188.68181 Bouajjani, Ahmed; Bozga, Marius; Habermehl, Peter; Iosif, Radu; Moro, Pierre; Vojnar, Tomáš 24 2006 Abstract regular tree model checking of complex dynamic data structures. Zbl 1225.68067 Bouajjani, Ahmed; Habermehl, Peter; Rogalewicz, Adam; Vojnar, Tomáš 23 2006 Abstract regular tree model checking. Zbl 1273.68221 Bouajjani, Ahmed; Habermehl, Peter; Rogalewicz, Adam; Vojnar, Tomáš 18 2006 A logic of reachable patterns in linked data-structures. Zbl 1180.68131 Yorsh, Greta; Rabinovich, Alexander; Sagiv, Mooly; Meyer, Antoine; Bouajjani, Ahmed 14 2006 Rewriting models of Boolean programs. Zbl 1151.68440 Bouajjani, Ahmed; Esparza, Javier 4 2006 Regular symbolic analysis of dynamic networks of pushdown systems. Zbl 1134.68427 Bouajjani, Ahmed; Müller-Olm, Markus; Touili, Tayssir 24 2005 Checking timed Büchi automata emptiness efficiently. Zbl 1085.68083 Tripakis, Stavros; Yovine, Sergio; Bouajjani, Ahmed 21 2005 Reachability analysis of multithreaded software with asynchronous communication. Zbl 1172.68422 Bouajjani, Ahmed; Esparza, Javier; Schwoon, Stefan; Strejček, Jan 16 2005 Verifying programs with dynamic 1-selector-linked structures in regular model checking. Zbl 1087.68585 Bouajjani, Ahmed; Habermehl, Peter; Moro, Pierre; Vojnar, Tomáš 12 2005 On computing reachability sets of process rewrite systems. Zbl 1078.68652 Bouajjani, Ahmed; Touili, Tayssir 12 2005 Handling liveness properties in (\(\omega\)-)regular model checking. Zbl 1272.68227 Bouajjani, Ahmed; Legay, Axel; Wolper, Pierre 5 2005 Reachability analysis of synchronized PA systems. Zbl 1272.68290 Bouajjani, Ahmed; Esparza, Javier; Touili, Tayssir 4 2005 Using forward reachability analysis for verification of lossy channel systems. Zbl 1073.68675 Abdulla, Parosh Aziz; Collomb-Annichini, Aurore; Bouajjani, Ahmed; Jonsson, Bengt 33 2004 Abstract regular model checking. Zbl 1103.68071 Bouajjani, Ahmed; Habermehl, Peter; Vojnar, Tomáš 28 2004 Symbolic reachability analysis of higher-order context-free processes. Zbl 1117.68395 Bouajjani, Ahmed; Meyer, Antoine 4 2004 A generic approach to the static analysis of concurrent programs with procedures. Zbl 1321.68185 Bouajjani, Ahmed; Esparza, Javier; Touili, Tayssir 23 2003 Reachability analysis of process rewrite systems. Zbl 1205.68183 Bouajjani, Ahmed; Touili, Tayssir 13 2003 Deciding monotonic games. Zbl 1116.68491 Abdulla, Parosh Aziz; Bouajjani, Ahmed; d’Orso, Julien 12 2003 A generic approach to the static analysis of concurrent programs with procedures. Zbl 1101.68457 Bouajjani, Ahmed; Esparza, Javier; Touili, Tayssir 11 2003 Automatic verification of recursive procedures with one integer parameter. Zbl 1053.68060 Bouajjani, Ahmed; Habermehl, Peter; Mayr, Richard 7 2003 Extrapolating tree transformations. Zbl 1010.68085 Bouajjani, Ahmed; Touili, Tayssir 10 2002 Parametric verification of a group membership algorithm. Zbl 1278.68159 Bouajjani, Ahmed; Merceron, Agathe 1 2002 TREX: A tool for reachability analysis of complex systems. Zbl 0991.68645 Annichini, Aurore; Bouajjani, Ahmed; Sighireanu, Mihaela 16 2001 Languages, rewriting systems, and verification of infinite-state systems. Zbl 0986.68517 Bouajjani, Ahmed 6 2001 Effective lossy queue languages. Zbl 0986.68044 Aziz Abdulla, Parosh; Boasson, Luc; Bouajjani, Ahmed 6 2001 Automatic verification of recursive procedures with one integer parameter. Zbl 1005.68096 Bouajjani, Ahmed; Habermehl, Peter; Mayr, Richard 1 2001 Regular model checking. Zbl 0974.68118 Bouajjani, Ahmed; Jonsson, Bengt; Nilsson, Marcus; Touili, Tayssir 44 2000 Symbolic techniques for parametric reasoning about counter and clock systems. Zbl 0974.68523 Annichini, Aurore; Asarin, Eugene; Bouajjani, Ahmed 10 2000 An efficient automata approach to some problems on context-free grammars. Zbl 1137.68418 Bouajjani, Ahmed; Esparza, Javier; Finkel, Alain; Maler, Oded; Rossmanith, Peter; Willems, Bernard; Wolper, Pierre 2 2000 Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Zbl 0933.68089 Bouajjani, Ahmed; Habermehl, Peter 21 1999 Handling global conditions in parameterized system verification. Zbl 1046.68573 Abdulla, Parosh Aziz; Bouajjani, Ahmed; Jonsson, Bengt; Nilsson, Marcus 17 1999 Model checking lossy vector addition systems. Zbl 0926.03035 Bouajjani, Ahmed; Mayr, Richard 12 1999 Reachability analysis of pushdown automata: application to model-checking. Zbl 1512.68135 Bouajjani, Ahmed; Esparza, Javier; Maler, Oded 102 1997 Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Zbl 1401.68186 Bouajjani, Ahmed; Habermehl, Peter 6 1997 Constrained properties, semilinear systems, and Petri nets. Zbl 1514.68125 Bouajjani, Ahmed; Habermehl, Peter 13 1996 Property preserving abstractions for the verification of concurrent systems. Zbl 0829.68053 Loiseaux, C.; Graf, S.; Sifakis, J.; Bouajjani, A.; Bensalem, S. 44 1995 Minimal state graph generation. Zbl 0769.68090 Bouajjani, A.; Fernandez, J.-C.; Halbwachs, N.; Raymond, P.; Ratel, C. 3 1992 Safety for branching time semantics. Zbl 0769.68089 Bouajjani, A.; Fernandez, J. C.; Graf, S.; Rodriguez, C.; Sifakis, J. 20 1991 Minimal model generation. Zbl 0765.68114 Bouajjani, A.; Fernandez, J.-C.; Halbwachs, N. 13 1991 Minimal model generation. Zbl 0786.68056 Bouajjani, A.; Fernandez, J.-C.; Halbwachs, N. 1 1991 A logic for the description of behaviors and properties of concurrent systems. (Technical contribution). Zbl 0683.68012 Bouajjani, A.; Graf, S.; Sifkis, J. 1 1989 all cited Publications top 5 cited Publications all top 5 Cited by 928 Authors 38 Bouajjani, Ahmed 28 Abdulla, Parosh Aziz 22 Atig, Mohamed Faouzi 19 Enea, Constantin 19 Finkel, Alain 19 Touili, Tayssir 14 Esparza, Javier 14 Vojnar, Tomáš 13 Habermehl, Peter 13 Lozes, Etienne 11 Holík, Lukáš 11 Majumdar, Rupak 11 Mayr, Richard M. 11 Schnoebelen, Philippe 10 Bollig, Benedikt 10 Henzinger, Thomas A. 10 Kucera, Antonin 9 Bozzelli, Laura 9 Demri, Stéphane P. 9 Zetzsche, Georg 8 Alur, Rajeev 8 Ganty, Pierre 8 Ibarra, Oscar H. 8 Meyer, Roland 8 Praveen, M. 8 Saivasan, Prakash 7 Emmi, Michael 7 Hamza, Jad 7 Iosif, Radu 7 Kupferman, Orna 7 Kuske, Dietrich 7 Lang, Frédéric 7 Madhusudan, Parthasarathy 7 Norman, Gethin 7 Raskin, Jean-François 7 Reps, Thomas W. 7 Schmitz, Sylvain 6 Di Giusto, Cinzia 6 Dongol, Brijesh 6 Héam, Pierre-Cyrille 6 Jacquemard, Florent 6 La Torre, Salvatore 6 Lal, Akash 6 Lengál, Ondřej 6 Leroux, Jérôme 6 Lin, Anthony Widjaja 6 Parlato, Gennaro 6 Qadeer, Shaz 6 Seidl, Helmut 5 Chatterjee, Krishnendu 5 Chiari, Michele 5 Dang, Zhe 5 Figueira, Diego 5 Godbole, Adwait Amit 5 Kwiatkowska, Marta Z. 5 Meseguer Guaita, José 5 Müller-Olm, Markus 5 Ouaknine, Joel O. 5 Pnueli, Amir 5 Podelski, Andreas 5 Pradella, Matteo 5 Rezine, Ahmed 5 Smith, Graeme 5 Wehrheim, Heike 5 Widder, Josef 4 André, Étienne 4 Beillahi, Sidi Mohamed 4 Boichut, Yohan 4 Bozga, Marius 4 Brochenin, Rémi 4 Bultan, Tevfik 4 Czerwiński, Wojciech 4 Farzan, Azadeh 4 Grumberg, Orna 4 Hague, Matthew 4 Hoffmann, Stefan 4 Hofman, Piotr 4 Jonsson, Bengt 4 Kiefer, Stefan 4 Konnov, Igor Vladimirovich 4 Lange, Martin 4 Larsen, Kim Guldstrand 4 Lazić, Ranko 4 Luttenberger, Michael 4 Mandrioli, Dino 4 Muskalla, Sebastian 4 Niskanen, Reino 4 Parker, David J. 4 Pavlogiannis, Andreas 4 Peron, Adriano 4 Potapov, Igor 4 Rakamarić, Zvonimir 4 Rogalewicz, Adam 4 Rümmer, Philipp 4 Sagiv, Mooly 4 Santone, Antonella 4 Sproston, Jeremy 4 Srba, Jiří 4 Sutre, Grégoire 4 Trivedi, Ashutosh ...and 828 more Authors all top 5 Cited in 40 Serials 74 Theoretical Computer Science 50 Information and Computation 35 Formal Methods in System Design 21 Logical Methods in Computer Science 16 Acta Informatica 15 Formal Aspects of Computing 14 Journal of Computer and System Sciences 10 International Journal of Foundations of Computer Science 8 Journal of Automated Reasoning 8 Journal of Logical and Algebraic Methods in Programming 7 Information Processing Letters 6 Theory of Computing Systems 6 The Journal of Logic and Algebraic Programming 6 ACM Transactions on Computational Logic 3 Artificial Intelligence 3 Computing 3 Journal of Computer Science and Technology 3 Real-Time Systems 3 Fundamenta Informaticae 2 Science of Computer Programming 2 Annals of Pure and Applied Logic 2 Journal of Symbolic Computation 2 Mathematical Structures in Computer Science 2 Journal of Applied Non-Classical Logics 2 Theory and Practice of Logic Programming 1 ACM Computing Surveys 1 International Journal of General Systems 1 Problems of Information Transmission 1 Automatica 1 Journal of Complexity 1 Algorithmica 1 Annals of Mathematics and Artificial Intelligence 1 Journal of Automata, Languages and Combinatorics 1 Higher-Order and Symbolic Computation 1 RAIRO. Theoretical Informatics and Applications 1 Computer Languages, Systems & Structures 1 Science in China. Series F 1 Science China. Information Sciences 1 Computer Science Review 1 ACM Transactions on Computation Theory all top 5 Cited in 18 Fields 646 Computer science (68-XX) 123 Mathematical logic and foundations (03-XX) 26 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 7 Systems theory; control (93-XX) 6 Combinatorics (05-XX) 4 Order, lattices, ordered algebraic structures (06-XX) 3 Associative rings and algebras (16-XX) 3 Probability theory and stochastic processes (60-XX) 3 Information and communication theory, circuits (94-XX) 2 Group theory and generalizations (20-XX) 2 Numerical analysis (65-XX) 2 Operations research, mathematical programming (90-XX) 1 General and overarching topics; collections (00-XX) 1 Category theory; homological algebra (18-XX) 1 Ordinary differential equations (34-XX) 1 General topology (54-XX) 1 Statistics (62-XX) 1 Biology and other natural sciences (92-XX) Citations by Year