×
Author ID: bouajjani.ahmed Recent zbMATH articles by "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

Publications by Year

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 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

Citations by Year