×

Clarke, Edmund Melson jun. (b. 1945 d. 2020)

Author ID: clarke.edmund-melson-jun Recent zbMATH articles by "Clarke, Edmund Melson jun."
Published as: Clarke, Edmund; Clarke, Edmund M.; Clarke, E. M.; Clarke, E.; Clarke, Edmund M. jun.; Clarke, Edmund Melson jun.; Clarke, E. M. jun.; Clarke, Edmund Melson
External Links: MGP · Wikidata · Google Scholar · dblp · GND · IdRef
Awards: Turing Award (2007)
all top 5

Co-Authors

8 single-authored
14 Grumberg, Orna
14 Veith, Helmut
11 Chaki, Sagar
8 Sharygina, Natasha
7 Jha, Somesh
7 Ouaknine, Joel O.
7 Sinha, Nishant
6 Browne, Michael C.
6 Emerson, Ernest Allen
6 Gao, Sicun
6 Kröning, Daniel
6 Kurshan, Robert P.
6 Platzer, André
6 Talupur, Muralidhar
6 Zuliani, Paolo
5 Biere, Armin
5 Krogh, Bruce H.
5 Wang, Dong
4 Henzinger, Thomas A.
4 Jain, Himanshu
4 Long, David E.
4 Mishra, Bud
4 Sistla, Aravinda Prasad
4 Strichman, Ofer
4 Yorav, Karen
4 Zhu, Yunshan
3 Baier, Christel
3 Cimatti, Alessandro
3 Dill, David L.
3 Fehnker, Ansgar
3 German, Steven M.
3 Giunchiglia, Fausto
3 Halpern, Joseph Yehuda
3 Klieber, William
3 Kukula, James H.
3 Lerda, Flavio
3 Lu, Yuan
3 Minea, Marius
3 Peled, Doron A.
3 Roveri, Marco
3 Touili, Tayssir
3 Zhao, Xudong
2 Avigad, Jeremy
2 Bose, Soumitra
2 Campos, Sérgio V. A.
2 Černý, Pavol
2 Chauhan, Pankaj
2 Chen, Yu-Fang
2 Draghicescu, I. A.
2 Farzan, Azadeh
2 Groce, Alex
2 Gupta, Anubhav
2 Han, Zhi
2 Hartonas-Garmhausen, Vasiliki
2 Janota, Mikoláš
2 Jha, Sumit Kumar
2 Komuravelli, Anvesh
2 Kong, Soonho
2 Marques-Silva, João P.
2 Marrero, Will
2 McMillan, Kenneth L.
2 Meyer, Albert Ronald
2 Michaylov, Spiro
2 Radhakrishna, Arjun
2 Raimi, Richard
2 Ryzhyk, Leonid
2 Samanta, Roopsha
2 Sapra, Samir
2 Stursberg, Olaf
2 Tarrach, Thorsten
2 Theobald, Michael
2 Tsay, Yih-Kuen
2 Voronkov, Andrei
2 Wang, Bow-Yaw
1 Aczel, Peter
1 Aguiar Campos, Sérgio Vale
1 Aho, Alfred Vaino
1 Anantharaman, T. S.
1 Andler, Sten F.
1 Andrews, Gregory R.
1 Bae, Kyungmin
1 Banning, John
1 Bartzis, Constantinos
1 Bauer, Andrej
1 Berdine, Josh
1 Berezin, Sergey
1 Bernstein, Philip A.
1 Bloem, Roderick
1 Browne, I. A.
1 Burch, Jerry R.
1 Cartwright, Robert
1 Casanova, Marco Antonio
1 Cohen, Norman H.
1 Cohen, Richard M.
1 Cohen, Rina S.
1 Constable, Robert Lee
1 Cook, Byron
1 Cousot, Patrick
1 Cousot, Radhia
1 Critcher, Adrienne
...and 63 more Co-Authors

Publications by Year

Citations contained in zbMATH Open

125 Publications have been cited 2,968 times in 1,986 Documents Cited by Year
Automatic verification of finite-state concurrent systems using temporal logic specifications. Zbl 0591.68027
Clarke, E. M.; Emerson, E. A.; Sistla, A. P.
323
1986
Design and synthesis of synchronization skeletons using branching time temporal logic. Zbl 0546.68014
Clarke, Edmund M.; Emerson, E. Allen
250
1982
The complexity of propositional linear temporal logics. Zbl 0632.68034
Sistla, A. P.; Clarke, E. M.
235
1985
Symbolic model checking: \(10^{20}\) states and beyond. Zbl 0753.68066
Burch, J. R.; Clarke, E. M.; McMillan, K. L.; Dill, D. L.; Hwang, L. J.
200
1992
Counterexample-guided abstraction refinement. Zbl 0974.68517
Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut
167
2000
Counterexample-guided abstraction refinement for symbolic model checking. Zbl 1325.68145
Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut
124
2003
NuSMV 2: An OpenSource tool for symbolic model checking. Zbl 1010.68766
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando
114
2002
Using branching time temporal logic to synthesize synchronization skeletons. Zbl 0514.68032
Emerson, E. Allen; Clarke, Edmund M.
85
1982
A tool for checking ANSI-C programs. Zbl 1126.68470
Clarke, Edmund; Kroening, Daniel; Lerda, Flavio
79
2004
Model checking. 2nd expanded and updated edition. Zbl 1423.68002
Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut
76
2018
Bounded model checking using satisfiability solving. Zbl 0985.68038
Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan
72
2001
Characterizing finite Kripke structures in propositional temporal logic. Zbl 0677.03011
Browne, M. C.; Clarke, E. M.; Grümberg, O.
70
1988
Handbook of model checking. Zbl 1390.68001
56
2018
Characterizing correctness properties of parallel programs using fixpoints. Zbl 0456.68016
Emerson, E. Allen; Clarke, Edmund M.
52
1980
NuSMV: A new symbolic model checker. Zbl 1059.68582
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco
47
2000
dReal: an SMT solver for nonlinear theories over the reals. Zbl 1381.68268
Gao, Sicun; Kong, Soonho; Clarke, Edmund M.
43
2013
Model checking. Zbl 0847.68063
Clarke, E.; Grumberg, O.; Long, D.
40
1996
NuSMV: A new symbolic model verifier. Zbl 1046.68587
Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M.
37
1999
Programming language constructs for which it is impossible to obtain good Hoare axiom systems. Zbl 0388.68008
Clarke, Edmund Melson jun.
33
1979
Solving QBF with counterexample guided refinement. Zbl 1273.68178
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
29
2012
Reasoning about networks with many identical finite state processes. Zbl 0709.68610
Browne, M. C.; Clarke, E. M.; Grumberg, O.
29
1989
Verifying safety properties of a PowerPC\(^{TM}\) microprocessor using symbolic model checking without BDDs. Zbl 1046.68578
Biere, Armin; Clarke, Edmund; Raimi, Richard; Zhu, Yunshan
29
1999
An improved algorithm for the evaluation of fixpoint expressions. Zbl 0901.68118
Browne, A.; Clarke, E. M.; Jha, S.; Long, D. E.; Marrero, W.
26
1997
Abstraction and counterexample-guided refinement in model checking of hybrid systems. Zbl 1101.68678
Clarke, Edmund; Fehnker, Ansgar; Han, Zhi; Krogh, Bruce; Ouaknine, Joël; Stursberg, Olaf; Theobald, Michael
25
2003
Extending automated compositional verification to the full class of omega-regular languages. Zbl 1134.68406
Farzan, Azadeh; Chen, Yu-Fang; Clarke, Edmund M.; Tsay, Yih-Kuen; Wang, Bow-Yaw
24
2008
Compositional model checking. Zbl 0716.68035
Clarke, E. M.; Long, D. E.; McMillan, K. L.
24
1989
Solving QBF with counterexample guided refinement. Zbl 1351.68254
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
23
2016
\(\delta \)-complete decision procedures for satisfiability over the reals. Zbl 1358.03028
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
22
2012
Symbolic model checking for probabilistic processes. Zbl 1401.68180
Baier, Christel; Clarke, Edmund M.; Hartonas-Garmhausen, Vasiliki; Kwiatkowska, Marta; Ryan, Mark
22
1997
Learning minimal separating DFA’s for compositional verification. Zbl 1234.68166
Chen, Yu-Fang; Farzan, Azadeh; Clarke, Edmund M.; Tsay, Yih-Kuen; Wang, Bow-Yaw
21
2009
SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
21
2005
Verifying concurrent message-passing C programs with recursive calls. Zbl 1180.68109
Chaki, S.; Clarke, E.; Kidd, N.; Reps, T.; Touili, T.
20
2006
Computing differential invariants of hybrid systems as fixedpoints. Zbl 1155.68445
Platzer, André; Clarke, Edmund M.
19
2008
Logic in computer science: Modelling and reasoning about systems. With a foreword by Edmund M. Clarke. Zbl 0955.68001
Huth, Michael; Ryan, Mark
19
2000
A non-prenex, non-clausal QBF solver with game-state learning. Zbl 1306.68161
Klieber, William; Sapra, Samir; Gao, Sicun; Clarke, Edmund
19
2010
State space reduction using partial order techniques. Zbl 1065.68506
Clarke, E. M.; Grumberg, O.; Minea, M.; Peled, D.
18
1999
Completeness and complexity of bounded model checking. Zbl 1202.68244
Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer
17
2004
Automatic verification of sequential circuits using temporal logic. Zbl 0604.94011
Browne, Michael C.; Clarke, Edmund M.; Dill, David L.; Mishra, Bud
17
1986
Automated assume-guarantee reasoning for simulation conformance. Zbl 1081.68612
Chaki, Sagar; Clarke, Edmund; Sinha, Nishant; Thati, Prasanna
16
2005
Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
16
2004
Verification by network decomposition. Zbl 1099.68653
Clarke, Edmund; Talupur, Muralidhar; Touili, Tayssir; Veith, Helmut
16
2004
Environment abstraction for parameterized verification. Zbl 1176.68117
Clarke, Edmund; Talupur, Muralidhar; Veith, Helmut
16
2006
The image computation problem in hybrid systems model checking. Zbl 1221.93118
Platzer, André; Clarke, Edmund M.
15
2007
The birth of model checking. Zbl 1142.68046
Clarke, Edmund M.
14
2008
State/event-based software model checking. Zbl 1196.68129
Chaki, Sagar; Clarke, Edmund M.; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant
14
2004
Verification of hybrid systems based on counterexample-guided abstraction refinement. Zbl 1031.68078
Clarke, Edmund; Fehnker, Ansgar; Han, Zhi; Krogh, Bruce; Stursberg, Olaf; Theobald, Michael
13
2003
Effective axiomatizations of Hoare logics. Zbl 0627.68010
Clarke, Edmund M. jun.; German, Steven M.; Halpern, Joseph Y.
11
1983
Expressibility results for linear-time and branching-time logics. (Technical contribution). Zbl 0683.68030
Clarke, E. M.; Drăghicescu, I. A.
11
1989
Analytica — an experiment in combining theorem proving and symbolic computation. Zbl 0916.68143
Bauer, Andrej; Clarke, Edmund; Zhao, Xudong
11
1998
Proving Ptolemy right: The environment abstraction framework for model checking concurrent systems. Zbl 1134.68403
Clarke, Edmund; Talupur, Murali; Veith, Helmut
10
2008
SAT based abstraction-refinement using ILP and machine learning techniques. Zbl 1010.68515
Clarke, Edmund; Gupta, Anubhav; Kukula, James; Strichman, Ofer
10
2002
Computing differential invariants of hybrid systems as fixed points. Zbl 1180.93024
Platzer, André; Clarke, Edmund M.
10
2009
Characterizing Kripke structures in temporal logic. Zbl 0626.03019
Browne, M. C.; Clarke, E. M.; Grümberg, O.
9
1987
Program invariants as fixedpoints. Zbl 0399.68022
Clarke, E. M.
9
1979
Efficient Craig interpolation for linear diophantine (dis)equations and linear modular equations. Zbl 1155.68439
Jain, Himanshu; Clarke, Edmund; Grumberg, Orna
9
2008
Hierarchical verification of asynchronous circuits using temporal logic. Zbl 0584.94022
Mishra, B.; Clarke, E.
9
1985
Statistical model checking for cyber-physical systems. Zbl 1348.68128
Clarke, Edmund M.; Zuliani, Paolo
8
2011
Design and synthesis of synchronization skeletons using branching time temporal logic. Zbl 1142.68431
Clarke, Edmund M.; Emerson, E. Allen
8
2008
Software reliability methods. Foreword by Edmund M. Clarke. Zbl 0980.68014
Peled, Doron A.
8
2001
Model checking. Zbl 1066.68075
Clarke, Edmund M.; Schlingloff, Bernd-Holger
8
2001
Reachability for linear hybrid automata using iterative relaxation abstraction. Zbl 1221.93115
Jha, Sumit K.; Krogh, Bruce H.; Weimer, James E.; Clarke, Edmund M.
8
2007
Concurrent software verification with states, events, and deadlocks. Zbl 1103.68609
Chaki, Sagar; Clarke, Edmund; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant
8
2005
Bayesian statistical model checking with application to Simulink/Stateflow verification. Zbl 1361.68154
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
8
2010
Bayesian statistical model checking with application to Stateflow/Simulink verification. Zbl 1291.68273
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
8
2013
Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. Zbl 1019.68618
Chauhan, Pankaj; Clarke, Edmund; Kukula, James; Sapra, Samir; Veith, Helmut; Wang, Dong
7
2002
SAT-based compositional verification using lazy learning. Zbl 1135.68483
Sinha, Nishant; Clarke, Edmund
7
2007
\(\delta\)-decidability over the reals. Zbl 1364.03065
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
7
2012
Counterexamples revisited: principles, algorithms, applications. Zbl 1274.68179
Clarke, Edmund; Veith, Helmut
6
2003
Dynamic component substitutability analysis. Zbl 1120.68421
Sharygina, Natasha; Chaki, Sagar; Clarke, Edmund; Sinha, Nishant
6
2005
Combining decision diagrams and SAT procedures for efficient symbolic model checking. Zbl 0974.68526
Williams, Poul F.; Biere, Armin; Clarke, Edmund M.; Gupta, Anubhav
6
2000
SAT based predicate abstraction for hardware verification. Zbl 1204.68129
Clarke, Edmund; Talupur, Muralidhar; Veith, Helmut; Wang, Dong
6
2004
Arithmetic strengthening for shape analysis. Zbl 1211.68094
Magill, Stephen; Berdine, Josh; Clarke, Edmund; Cook, Byron
6
2007
Can message buffers be axiomatized in linear temporal logic? Zbl 0591.68022
Sistla, A. P.; Clarke, E. M.; Francez, N.; Meyer, A. R.
6
1984
Refining abstractions of hybrid systems using counterexample fragments. Zbl 1078.93041
Fehnker, Ansgar; Clarke, Edmund; Jha, Sumit Kumar; Krogh, Bruce
6
2005
Verification of supervisory control software using state proximity and merging. Zbl 1143.68457
Lerda, Flavio; Kapinski, James; Clarke, Edmund M.; Krogh, Bruce H.
6
2008
A unified approach for showing language inclusion and equivalence between various types of \(\omega\)-automata. Zbl 0925.68274
Clarke, E. M.; Draghicescu, I. A.; Kurshan, R. P.
5
1993
Parthenon: A parallel theorem prover for non-Horn clauses. Zbl 0716.68076
Bose, Soumitra; Clarke, Edmund M.; Long, David E.; Michaylov, Spiro
5
1989
A synthesis of two approaches for verifying finite state concurrent systems. Zbl 0688.68019
Clarke, E. M.; Grumberg, O.; Kurshan, R. P.
5
1989
Learning probabilistic systems from tree samples. Zbl 1362.68122
Komuravelli, Anvesh; Păsăreanu, Corina S.; Clarke, Edmund M.
5
2012
Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 – May 1, 2010. Revised selected papers. Zbl 1203.68004
4
2010
State/event software verification for branching-time specifications. Zbl 1137.68432
Chaki, Sagar; Clarke, Edmund; Grumberg, Orna; Ouaknine, Joël; Sharygina, Natasha; Touili, Tayssir; Veith, Helmut
4
2005
Synthesis of resource invariants for concurrent programs. Zbl 0468.68024
Clarke, Edmund Melson jun.
4
1980
Statistical verification of probabilistic properties with unbounded until. Zbl 1325.68158
Younes, Håkan L. S.; Clarke, Edmund M.; Zuliani, Paolo
4
2011
Reasoning about procedures as parameters in the language L4. Zbl 0692.68011
German, Steven M.; Clarke, Edmund M.; Halpern, Joseph Y.
4
1989
Verification of SpecC using predicate abstraction. Zbl 1117.68046
Clarke, Edmund; Jain, Himanshu; Kroening, Daniel
4
2007
Analysis and verification of real-time systems using quantitative symbolic algorithms. Zbl 1065.68505
Aguiar Campos, Sérgio Vale; Clarke, Edmund
4
1999
On simulation-based probabilistic model checking of mixed-analog circuits. Zbl 1207.68205
Clarke, Edmund; Donzé, Alexandre; Legay, Axel
4
2010
Verification of evolving software via component substitutability analysis. Zbl 1147.68047
Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant
4
2008
From non-preemptive to preemptive scheduling using synchronization synthesis. Zbl 1381.68040
Černý, Pavol; Clarke, Edmund M.; Henzinger, Thomas A.; Radhakrishna, Arjun; Ryzhyk, Leonid; Samanta, Roopsha; Tarrach, Thorsten
4
2015
Rare-event verification for stochastic hybrid systems. Zbl 1362.68192
Zuliani, Paolo; Baier, Christel; Clarke, Edmund M.
4
2012
Automated compositional abstraction refinement for concurrent C programs: a two-level approach. Zbl 1271.68081
Chaki, Sagar; Ouaknine, Joël; Yorav, Karen; Clarke, Edmund
3
2003
Computational modeling and verification of signaling pathways in cancer. Zbl 1349.92074
Gong, Haijun; Zuliani, Paolo; Komuravelli, Anvesh; Faeder, James R.; Clarke, Edmund M.
3
2012
Partial order reductions for security protocol verification. Zbl 0965.68053
Clarke, Edmund; Jha, Somesh; Marrero, Will
3
2000
SMT-based analysis of virtually synchronous distributed hybrid systems. Zbl 1364.68258
Bae, Kyungmin; Ölveczky, Peter Csaba; Kong, Soonho; Gao, Sicun; Clarke, Edmund M.
3
2016
Reasoning about procedures as parameters. Zbl 0539.68010
German, S. M.; Clarke, E. M. jun.; Halpern, J. Y.
2
1984
Automatic verification of asynchronous circuits. Zbl 0541.94038
Clarke, E.; Mishra, B.
2
1984
A synthesis of two approaches for verifying finite state concurrent systems. Zbl 0782.68078
Clarke, E. M.; Grumberg, O.; Kurshan, R. P.
2
1992
Making predicate abstraction efficient: how to eliminate redundant predicates. Zbl 1278.68163
Clarke, Edmund; Grumberg, Orna; Talupur, Muralidhar; Wang, Dong
2
2003
A unified approach for showing language containment and equivalence between various types of \(\omega\)-automata. Zbl 0759.68063
Clarke, E. M.; Browne, I. A.; Kurshan, R. P.
2
1990
Satisfiability checking of non-clausal formulas using general matings. Zbl 1187.68549
Jain, Himanshu; Bartzis, Constantinos; Clarke, Edmund
2
2006
Model checking. 2nd expanded and updated edition. Zbl 1423.68002
Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut
76
2018
Handbook of model checking. Zbl 1390.68001
56
2018
Introduction to model checking. Zbl 1392.68242
Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut
1
2018
From non-preemptive to preemptive scheduling using synchronization synthesis. Zbl 1360.68346
Černý, Pavol; Clarke, Edmund M.; Henzinger, Thomas A.; Radhakrishna, Arjun; Ryzhyk, Leonid; Samanta, Roopsha; Tarrach, Thorsten
1
2017
Solving QBF with counterexample guided refinement. Zbl 1351.68254
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
23
2016
SMT-based analysis of virtually synchronous distributed hybrid systems. Zbl 1364.68258
Bae, Kyungmin; Ölveczky, Peter Csaba; Kong, Soonho; Gao, Sicun; Clarke, Edmund M.
3
2016
From non-preemptive to preemptive scheduling using synchronization synthesis. Zbl 1381.68040
Černý, Pavol; Clarke, Edmund M.; Henzinger, Thomas A.; Radhakrishna, Arjun; Ryzhyk, Leonid; Samanta, Roopsha; Tarrach, Thorsten
4
2015
\(2^{5}\) years of model checking. Zbl 1434.68296
Clarke, Edmund M.; Wang, Qinsi
2
2015
dReal: an SMT solver for nonlinear theories over the reals. Zbl 1381.68268
Gao, Sicun; Kong, Soonho; Clarke, Edmund M.
43
2013
Bayesian statistical model checking with application to Stateflow/Simulink verification. Zbl 1291.68273
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
8
2013
Solving QBF with counterexample guided refinement. Zbl 1273.68178
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
29
2012
\(\delta \)-complete decision procedures for satisfiability over the reals. Zbl 1358.03028
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
22
2012
\(\delta\)-decidability over the reals. Zbl 1364.03065
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
7
2012
Learning probabilistic systems from tree samples. Zbl 1362.68122
Komuravelli, Anvesh; Păsăreanu, Corina S.; Clarke, Edmund M.
5
2012
Rare-event verification for stochastic hybrid systems. Zbl 1362.68192
Zuliani, Paolo; Baier, Christel; Clarke, Edmund M.
4
2012
Computational modeling and verification of signaling pathways in cancer. Zbl 1349.92074
Gong, Haijun; Zuliani, Paolo; Komuravelli, Anvesh; Faeder, James R.; Clarke, Edmund M.
3
2012
Statistical model checking for cyber-physical systems. Zbl 1348.68128
Clarke, Edmund M.; Zuliani, Paolo
8
2011
Statistical verification of probabilistic properties with unbounded until. Zbl 1325.68158
Younes, Håkan L. S.; Clarke, Edmund M.; Zuliani, Paolo
4
2011
Quantifier elimination over finite fields using Gröbner bases. Zbl 1339.68321
Gao, Sicun; Platzer, André; Clarke, Edmund M.
1
2011
A non-prenex, non-clausal QBF solver with game-state learning. Zbl 1306.68161
Klieber, William; Sapra, Samir; Gao, Sicun; Clarke, Edmund
19
2010
Bayesian statistical model checking with application to Simulink/Stateflow verification. Zbl 1361.68154
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
8
2010
Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 – May 1, 2010. Revised selected papers. Zbl 1203.68004
4
2010
On simulation-based probabilistic model checking of mixed-analog circuits. Zbl 1207.68205
Clarke, Edmund; Donzé, Alexandre; Legay, Axel
4
2010
Learning minimal separating DFA’s for compositional verification. Zbl 1234.68166
Chen, Yu-Fang; Farzan, Azadeh; Clarke, Edmund M.; Tsay, Yih-Kuen; Wang, Bow-Yaw
21
2009
Computing differential invariants of hybrid systems as fixed points. Zbl 1180.93024
Platzer, André; Clarke, Edmund M.
10
2009
Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. Zbl 1186.68013
Jain, Himanshu; Clarke, Edmund M.; Grumberg, Orna
1
2009
Extending automated compositional verification to the full class of omega-regular languages. Zbl 1134.68406
Farzan, Azadeh; Chen, Yu-Fang; Clarke, Edmund M.; Tsay, Yih-Kuen; Wang, Bow-Yaw
24
2008
Computing differential invariants of hybrid systems as fixedpoints. Zbl 1155.68445
Platzer, André; Clarke, Edmund M.
19
2008
The birth of model checking. Zbl 1142.68046
Clarke, Edmund M.
14
2008
Proving Ptolemy right: The environment abstraction framework for model checking concurrent systems. Zbl 1134.68403
Clarke, Edmund; Talupur, Murali; Veith, Helmut
10
2008
Efficient Craig interpolation for linear diophantine (dis)equations and linear modular equations. Zbl 1155.68439
Jain, Himanshu; Clarke, Edmund; Grumberg, Orna
9
2008
Design and synthesis of synchronization skeletons using branching time temporal logic. Zbl 1142.68431
Clarke, Edmund M.; Emerson, E. Allen
8
2008
Verification of supervisory control software using state proximity and merging. Zbl 1143.68457
Lerda, Flavio; Kapinski, James; Clarke, Edmund M.; Krogh, Bruce H.
6
2008
Verification of evolving software via component substitutability analysis. Zbl 1147.68047
Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant
4
2008
The image computation problem in hybrid systems model checking. Zbl 1221.93118
Platzer, André; Clarke, Edmund M.
15
2007
Reachability for linear hybrid automata using iterative relaxation abstraction. Zbl 1221.93115
Jha, Sumit K.; Krogh, Bruce H.; Weimer, James E.; Clarke, Edmund M.
8
2007
SAT-based compositional verification using lazy learning. Zbl 1135.68483
Sinha, Nishant; Clarke, Edmund
7
2007
Arithmetic strengthening for shape analysis. Zbl 1211.68094
Magill, Stephen; Berdine, Josh; Clarke, Edmund; Cook, Byron
6
2007
Verification of SpecC using predicate abstraction. Zbl 1117.68046
Clarke, Edmund; Jain, Himanshu; Kroening, Daniel
4
2007
Verifying concurrent message-passing C programs with recursive calls. Zbl 1180.68109
Chaki, S.; Clarke, E.; Kidd, N.; Reps, T.; Touili, T.
20
2006
Environment abstraction for parameterized verification. Zbl 1176.68117
Clarke, Edmund; Talupur, Muralidhar; Veith, Helmut
16
2006
Satisfiability checking of non-clausal formulas using general matings. Zbl 1187.68549
Jain, Himanshu; Bartzis, Constantinos; Clarke, Edmund
2
2006
Program compatibility approaches. Zbl 1196.68044
Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant
1
2006
Verification of infinite-state systems with applications to security. Proceedings of the NATO Advanced Research Workshop on verification of infinite-state systems with applications to security, Timaşoara, Romania, March 17–22, 2005. Zbl 1126.68054
1
2006
SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
21
2005
Automated assume-guarantee reasoning for simulation conformance. Zbl 1081.68612
Chaki, Sagar; Clarke, Edmund; Sinha, Nishant; Thati, Prasanna
16
2005
Concurrent software verification with states, events, and deadlocks. Zbl 1103.68609
Chaki, Sagar; Clarke, Edmund; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant
8
2005
Dynamic component substitutability analysis. Zbl 1120.68421
Sharygina, Natasha; Chaki, Sagar; Clarke, Edmund; Sinha, Nishant
6
2005
Refining abstractions of hybrid systems using counterexample fragments. Zbl 1078.93041
Fehnker, Ansgar; Clarke, Edmund; Jha, Sumit Kumar; Krogh, Bruce
6
2005
State/event software verification for branching-time specifications. Zbl 1137.68432
Chaki, Sagar; Clarke, Edmund; Grumberg, Orna; Ouaknine, Joël; Sharygina, Natasha; Touili, Tayssir; Veith, Helmut
4
2005
A tool for checking ANSI-C programs. Zbl 1126.68470
Clarke, Edmund; Kroening, Daniel; Lerda, Flavio
79
2004
Completeness and complexity of bounded model checking. Zbl 1202.68244
Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer
17
2004
Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
16
2004
Verification by network decomposition. Zbl 1099.68653
Clarke, Edmund; Talupur, Muralidhar; Touili, Tayssir; Veith, Helmut
16
2004
State/event-based software model checking. Zbl 1196.68129
Chaki, Sagar; Clarke, Edmund M.; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant
14
2004
SAT based predicate abstraction for hardware verification. Zbl 1204.68129
Clarke, Edmund; Talupur, Muralidhar; Veith, Helmut; Wang, Dong
6
2004
Efficient verification of sequential and concurrent C programs. Zbl 1101.68677
Chaki, S.; Clarke, E.; Groce, A.; Ouaknine, J.; Strichman, O.; Yorav, K.
2
2004
Counterexample-guided abstraction refinement for symbolic model checking. Zbl 1325.68145
Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut
124
2003
Abstraction and counterexample-guided refinement in model checking of hybrid systems. Zbl 1101.68678
Clarke, Edmund; Fehnker, Ansgar; Han, Zhi; Krogh, Bruce; Ouaknine, Joël; Stursberg, Olaf; Theobald, Michael
25
2003
Verification of hybrid systems based on counterexample-guided abstraction refinement. Zbl 1031.68078
Clarke, Edmund; Fehnker, Ansgar; Han, Zhi; Krogh, Bruce; Stursberg, Olaf; Theobald, Michael
13
2003
Counterexamples revisited: principles, algorithms, applications. Zbl 1274.68179
Clarke, Edmund; Veith, Helmut
6
2003
Automated compositional abstraction refinement for concurrent C programs: a two-level approach. Zbl 1271.68081
Chaki, Sagar; Ouaknine, Joël; Yorav, Karen; Clarke, Edmund
3
2003
Making predicate abstraction efficient: how to eliminate redundant predicates. Zbl 1278.68163
Clarke, Edmund; Grumberg, Orna; Talupur, Muralidhar; Wang, Dong
2
2003
Predicate abstraction with minimum predicates. Zbl 1179.68033
Chaki, Sagar; Clarke, Edmund; Groce, Alex; Strichman, Ofer
1
2003
NuSMV 2: An OpenSource tool for symbolic model checking. Zbl 1010.68766
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando
114
2002
SAT based abstraction-refinement using ILP and machine learning techniques. Zbl 1010.68515
Clarke, Edmund; Gupta, Anubhav; Kukula, James; Strichman, Ofer
10
2002
Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. Zbl 1019.68618
Chauhan, Pankaj; Clarke, Edmund; Kukula, James; Sapra, Samir; Veith, Helmut; Wang, Dong
7
2002
Verification of out-of-order processor designs using model Checking and a light-weight completion function. Zbl 1014.68147
Berezin, Sergey; Clarke, Edmund; Biere, Armin; Zhu, Yunshan
1
2002
SAT-based counterexample guided abstraction refinement. Zbl 1077.68681
Clarke, Edmund M.
1
2002
Bounded model checking using satisfiability solving. Zbl 0985.68038
Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan
72
2001
Software reliability methods. Foreword by Edmund M. Clarke. Zbl 0980.68014
Peled, Doron A.
8
2001
Model checking. Zbl 1066.68075
Clarke, Edmund M.; Schlingloff, Bernd-Holger
8
2001
Using combinatorial optimization methods for quantification scheduling. Zbl 1002.68512
Chauhan, P.; Clarke, E.; Jha, S.; Kukula, J.; Veith, H.; Wang, D.
1
2001
The Verus language: Representing time efficiently with BDDs. Zbl 0954.68098
Campos, S. V. A.; Clarke, E.
1
2001
Counterexample-guided abstraction refinement. Zbl 0974.68517
Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut
167
2000
NuSMV: A new symbolic model checker. Zbl 1059.68582
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco
47
2000
Logic in computer science: Modelling and reasoning about systems. With a foreword by Edmund M. Clarke. Zbl 0955.68001
Huth, Michael; Ryan, Mark
19
2000
Combining decision diagrams and SAT procedures for efficient symbolic model checking. Zbl 0974.68526
Williams, Poul F.; Biere, Armin; Clarke, Edmund M.; Gupta, Anubhav
6
2000
Partial order reductions for security protocol verification. Zbl 0965.68053
Clarke, Edmund; Jha, Somesh; Marrero, Will
3
2000
NuSMV: A new symbolic model verifier. Zbl 1046.68587
Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M.
37
1999
Verifying safety properties of a PowerPC\(^{TM}\) microprocessor using symbolic model checking without BDDs. Zbl 1046.68578
Biere, Armin; Clarke, Edmund; Raimi, Richard; Zhu, Yunshan
29
1999
State space reduction using partial order techniques. Zbl 1065.68506
Clarke, E. M.; Grumberg, O.; Minea, M.; Peled, D.
18
1999
Analysis and verification of real-time systems using quantitative symbolic algorithms. Zbl 1065.68505
Aguiar Campos, Sérgio Vale; Clarke, Edmund
4
1999
Model checking semi-continuous time model using BDDS. Zbl 0920.68076
Campos, Sergio; Teixeira, Marcio; Minea, Marius; Kuehlmann, Andreas; Clarke, Edmund
1
1999
Abstract BDDs: A technique for using abstraction in model checking. Zbl 0949.68105
Clarke, Edmund; Jha, Somesh; Lu, Yuan; Wang, Dong
1
1999
Analytica — an experiment in combining theorem proving and symbolic computation. Zbl 0916.68143
Bauer, Andrej; Clarke, Edmund; Zhao, Xudong
11
1998
An improved algorithm for the evaluation of fixpoint expressions. Zbl 0901.68118
Browne, A.; Clarke, E. M.; Jha, S.; Long, D. E.; Marrero, W.
26
1997
Symbolic model checking for probabilistic processes. Zbl 1401.68180
Baier, Christel; Clarke, Edmund M.; Hartonas-Garmhausen, Vasiliki; Kwiatkowska, Marta; Ryan, Mark
22
1997
Model checking. Zbl 0847.68063
Clarke, E.; Grumberg, O.; Long, D.
40
1996
Multi-terminal binary decision diagrams and hybrid decision diagrams. Zbl 0855.94028
Clarke, Edmund M.; Fujita, Masahiro; Zhao, Xudong
1
1996
Combining symbolic computation and theorem proving: some problems of Ramanujan. Zbl 1433.68541
Clarke, Edmund; Zhao, Xudong
1
1994
A unified approach for showing language inclusion and equivalence between various types of \(\omega\)-automata. Zbl 0925.68274
Clarke, E. M.; Draghicescu, I. A.; Kurshan, R. P.
5
1993
Symbolic model checking: \(10^{20}\) states and beyond. Zbl 0753.68066
Burch, J. R.; Clarke, E. M.; McMillan, K. L.; Dill, D. L.; Hwang, L. J.
200
1992
A synthesis of two approaches for verifying finite state concurrent systems. Zbl 0782.68078
Clarke, E. M.; Grumberg, O.; Kurshan, R. P.
2
1992
PARTHENON: A parallel theorem prover for non-horn clauses. Zbl 0759.68079
Bose, Soumitra; Clarke, Edmund M.; Long, David E.; Michaylov, Spiro
1
1992
Computer-aided verification. 2nd international conference, CAV ’90, New Brunswick, NJ, USA, June 18–21, 1990. Proceedings. Zbl 0756.00006
1
1991
Temporal logic model checking: Two techniques for avoiding the state explosion problem. Zbl 0786.68058
Clarke, Edmund M. jun.
1
1991
Computer-aided verification ’90. Proceedings of a 2nd DIMACS workshop, June 18-21, 1990, Rutgers Univ., New Brunswick, NJ, USA. Zbl 0753.00020
1
1991
A unified approach for showing language containment and equivalence between various types of \(\omega\)-automata. Zbl 0759.68063
Clarke, E. M.; Browne, I. A.; Kurshan, R. P.
2
1990
Reasoning about networks with many identical finite state processes. Zbl 0709.68610
Browne, M. C.; Clarke, E. M.; Grumberg, O.
29
1989
...and 25 more Documents
all top 5

Cited by 3,084 Authors

35 Vardi, Moshe Ya’akov
29 Kupferman, Orna
27 Kröning, Daniel
25 Duan, Zhenhua
24 Clarke, Edmund Melson jun.
23 Murano, Aniello
22 Cimatti, Alessandro
21 Grumberg, Orna
20 Peled, Doron A.
20 Tian, Cong
19 Lange, Martin
18 Platzer, André
17 Baier, Christel
17 Henzinger, Thomas A.
16 Abdulla, Parosh Aziz
16 Zhang, Nan
14 Bozzelli, Laura
14 Katoen, Joost-Pieter
14 Larsen, Kim Guldstrand
14 Markey, Nicolas
14 Pnueli, Amir
13 Biere, Armin
13 Demri, Stéphane P.
13 Schewe, Sven
12 Tonetta, Stefano
12 Wooldridge, Michael J.
12 Zhang, Lijun
11 Abate, Alessandro
11 Finkbeiner, Bernd
11 Gutierrez, Julian
11 Kwiatkowska, Marta Z.
11 Laroussinie, François
11 Perelli, Giuseppe
11 Raskin, Jean-François
11 Reynolds, Mark Alexander
11 Roveri, Marco
11 Steffen, Bernhard
11 Zhan, Naijun
10 Brim, Luboš
10 Gnesi, Stefania
10 Griggio, Alberto
10 Legay, Axel
10 Sharygina, Natasha
10 Sifakis, Joseph
10 Touili, Tayssir
10 Veith, Helmut
9 Bouyer, Patricia
9 Dixon, Clare
9 Fisman, Dana
9 Gurfinkel, Arie
9 Jamroga, Wojciech
9 Konnov, Igor V.
9 Norman, Gethin
9 Zimmermann, Martin
8 Barrett, Clark W.
8 Beneš, Nikola
8 Beyersdorff, Olaf
8 Bloem, Roderick
8 Chatterjee, Krishnendu
8 Emerson, Ernest Allen
8 Järvisalo, Matti
8 Kamide, Norihiro
8 Martí-Oliet, Narciso
8 Peron, Adriano
8 Ratschan, Stefan
8 Seidl, Martina
8 Sorrentino, Loredana
7 Aceto, Luca
7 Atig, Mohamed Faouzi
7 Bolotov, Alexander
7 Dasgupta, Pallab
7 De Nicola, Rocco
7 Fantechi, Alessandro
7 French, Tim
7 Gheorghe, Marian
7 Halpern, Joseph Yehuda
7 Hermanns, Holger
7 Heule, Marijn J. H.
7 Ipate, Florentin
7 Konur, Savas
7 Leucker, Martin
7 Marques-Silva, João P.
7 McMillan, Kenneth L.
7 Meier, Arne
7 Mogavero, Fabio
7 Păsăreanu, Corina S.
7 Rabinovich, Alexander
7 Rümmer, Philipp
7 Rybakov, Vladimir Vladimirovich
7 Sebastiani, Roberto
7 Seshia, Sanjit Arunkumar
7 Smolka, Scott A.
7 Strichman, Ofer
7 Wolf, Karsten
7 Wolter, Frank
6 Angluin, Dana
6 Becker, Bernd
6 Bensalem, Saddek
6 Bonakdarpour, Borzoo
6 Bouajjani, Ahmed
...and 2,984 more Authors
all top 5

Cited in 141 Serials

197 Theoretical Computer Science
143 Formal Methods in System Design
104 Information and Computation
81 Formal Aspects of Computing
54 Artificial Intelligence
48 Acta Informatica
42 Journal of Automated Reasoning
30 Journal of Computer and System Sciences
29 The Journal of Logic and Algebraic Programming
28 Information Processing Letters
25 Journal of Logical and Algebraic Methods in Programming
24 Logical Methods in Computer Science
23 Science of Computer Programming
19 Journal of Applied Logic
17 Automatica
17 International Journal of Foundations of Computer Science
17 Annals of Mathematics and Artificial Intelligence
16 ACM Transactions on Computational Logic
15 Discrete Event Dynamic Systems
12 Annals of Pure and Applied Logic
12 Journal of Symbolic Computation
11 Distributed Computing
10 Journal of Computer Science and Technology
10 Journal of Applied Non-Classical Logics
10 Fundamenta Informaticae
9 Programming and Computer Software
9 MSCS. Mathematical Structures in Computer Science
8 Information Sciences
8 Studia Logica
8 Journal of Logic, Language and Information
8 European Journal of Control
8 Theory and Practice of Logic Programming
8 Journal of Applied Mathematics
7 Theory of Computing Systems
6 Nonlinear Analysis. Hybrid Systems
6 Modelirovanie i Analiz Informatsionnykh Sistem
5 Discrete Applied Mathematics
5 Constraints
5 Computer Languages, Systems & Structures
4 International Journal of Approximate Reasoning
4 Real-Time Systems
4 The Journal of Artificial Intelligence Research (JAIR)
4 The Bulletin of Symbolic Logic
4 RAIRO. Theoretical Informatics and Applications
4 Sādhanā
4 Science China. Information Sciences
3 Synthese
3 Algorithmica
3 International Journal of Applied Mathematics and Computer Science
3 Journal of Satisfiability, Boolean Modeling and Computation
3 Frontiers of Computer Science
3 Computer Science Review
2 International Journal of General Systems
2 BIT
2 Computing
2 Fuzzy Sets and Systems
2 Journal of Philosophical Logic
2 The Journal of Symbolic Logic
2 Notre Dame Journal of Formal Logic
2 SIAM Journal on Computing
2 Siberian Mathematical Journal
2 International Journal of Parallel Programming
2 Mathematical and Computer Modelling
2 Journal of Parallel and Distributed Computing
2 Machine Learning
2 JETAI. Journal of Experimental & Theoretical Artificial Intelligence
2 Automation and Remote Control
2 Cybernetics and Systems Analysis
2 Archives of Control Sciences
2 Journal of Combinatorial Optimization
2 Journal of the ACM
2 ACM Journal of Experimental Algorithmics
2 Science in China. Series F
2 Games
2 Journal of Membrane Computing
1 ACM Computing Surveys
1 Computers & Mathematics with Applications
1 Discrete Mathematics
1 International Journal of Control
1 International Journal of Theoretical Physics
1 Algebra and Logic
1 Calcolo
1 Journal of Mathematical Economics
1 Journal of Soviet Mathematics
1 Nonlinear Analysis. Theory, Methods & Applications. Series A: Theory and Methods
1 RAIRO, Informatique Théorique
1 Cybernetics
1 Systems & Control Letters
1 International Journal of Production Research
1 Order
1 New Generation Computing
1 Computers & Operations Research
1 MCSS. Mathematics of Control, Signals, and Systems
1 Games and Economic Behavior
1 Linear Algebra and its Applications
1 RAIRO. Informatique Théorique et Applications
1 Archive for Mathematical Logic
1 Applicable Algebra in Engineering, Communication and Computing
1 International Journal of Robust and Nonlinear Control
1 Foundations of Computing and Decision Sciences
...and 41 more Serials

Citations by Year

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.