×

zbMATH — the first resource for mathematics

Clarke, Edmund Melson jun.

Compute Distance To:
Author ID: clarke.edmund-melson-jun Recent zbMATH articles by "Clarke, Edmund Melson jun."
Published as: Clarke, Edmund M.; Clarke, Edmund; Clarke, E. M.; Clarke, E.; Clarke, Edmund M. jun.; Clarke, Edmund Melson jun.; Clarke, E. M. jun.; Clarke, Edmund Melson
Homepage: http://www.cs.cmu.edu/~emc/
External Links: MGP · Wikidata · dblp · GND
Awards: Turing Award (2007)
Documents Indexed: 132 Publications since 1979, including 8 Books
Biographic References: 1 Publication
all top 5

Co-Authors

9 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 Roveri, Marco
3 Touili, Tayssir
3 Zhao, Xudong
2 Avigad, Jeremy
2 Bose, Soumitra
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 Michaylov, Spiro
2 Peled, Doron A.
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 Aguiar Campos, Sérgio Vale
1 Anantharaman, T. S.
1 Bae, Kyungmin
1 Bartzis, Constantinos
1 Bauer, Andrej
1 Berdine, Josh
1 Berezin, Sergey
1 Bloem, Roderick
1 Browne, I. A.
1 Burch, Jerry R.
1 Campos, S. V. A.
1 Campos, Sergio
1 Cook, Byron
1 Donzé, Alexandre
1 Evans, Arthur jun.
1 Faeder, James R.
1 Foster, M. J.
1 Francez, Nissim
1 Fujita, Masahiro
1 Giunchiglia, Enrico
1 Gong, Haijun
1 Hwang, L. J.
1 Kapinski, James
1 Kidd, Nicholas
1 Kozen, Dexter C.
1 Kuehlmann, Andreas
1 Kwiatkowska, Marta Z.
1 Legay, Axel
...and 19 more Co-Authors

Publications by Year

Citations contained in zbMATH Open

114 Publications have been cited 1,938 times in 1,319 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.
247
1986
The complexity of propositional linear temporal logics. Zbl 0632.68034
Sistla, A. P.; Clarke, E. M.
176
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.
148
1992
Counterexample-guided abstraction refinement. Zbl 0974.68517
Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut
117
2000
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
78
2002
Counterexample-guided abstraction refinement for symbolic model checking. Zbl 1325.68145
Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut
73
2003
Design and synthesis of synchronization skeletons using branching time temporal logic. Zbl 0546.68014
Clarke, Edmund M.; Emerson, E. Allen
66
1982
Using branching time temporal logic to synthesize synchronization skeletons. Zbl 0514.68032
Emerson, E. Allen; Clarke, Edmund M.
65
1982
Characterizing finite Kripke structures in propositional temporal logic. Zbl 0677.03011
Browne, M. C.; Clarke, E. M.; Grümberg, O.
58
1988
A tool for checking ANSI-C programs. Zbl 1126.68470
Clarke, Edmund; Kroening, Daniel; Lerda, Flavio
56
2004
Bounded model checking using satisfiability solving. Zbl 0985.68038
Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan
47
2001
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.
34
1999
Characterizing correctness properties of parallel programs using fixpoints. Zbl 0456.68016
Emerson, E. Allen; Clarke, Edmund M.
33
1980
NuSMV: A new symbolic model checker. Zbl 1059.68582
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco
32
2000
Programming language constructs for which it is impossible to obtain good Hoare axiom systems. Zbl 0388.68008
Clarke, Edmund Melson jun.
28
1979
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
23
1999
Reasoning about networks with many identical finite state processes. Zbl 0709.68610
Browne, M. C.; Clarke, E. M.; Grumberg, O.
22
1989
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
20
2003
SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
20
2005
Solving QBF with counterexample guided refinement. Zbl 1273.68178
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
20
2012
Compositional model checking. Zbl 0716.68035
Clarke, E. M.; Long, D. E.; McMillan, K. L.
19
1989
Symbolic model checking for probabilistic processes. Zbl 1401.68180
Baier, Christel; Clarke, Edmund M.; Hartonas-Garmhausen, Vasiliki; Kwiatkowska, Marta; Ryan, Mark
17
1997
dReal: an SMT solver for nonlinear theories over the reals. Zbl 1381.68268
Gao, Sicun; Kong, Soonho; Clarke, Edmund M.
17
2013
An improved algorithm for the evaluation of fixpoint expressions. Zbl 0901.68118
Browne, A.; Clarke, E. M.; Jha, S.; Long, D. E.; Marrero, W.
16
1997
Model checking. 2nd expanded and updated edition. Zbl 1423.68002
Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut
15
2018
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
14
2008
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
13
2009
Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
13
2004
State/event-based software model checking. Zbl 1196.68129
Chaki, Sagar; Clarke, Edmund M.; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant
13
2004
Completeness and complexity of bounded model checking. Zbl 1202.68244
Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer
13
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
12
2003
Verification by network decomposition. Zbl 1099.68653
Clarke, Edmund; Talupur, Muralidhar; Touili, Tayssir; Veith, Helmut
12
2004
Computing differential invariants of hybrid systems as fixedpoints. Zbl 1155.68445
Platzer, André; Clarke, Edmund M.
12
2008
A non-prenex, non-clausal QBF solver with game-state learning. Zbl 1306.68161
Klieber, William; Sapra, Samir; Gao, Sicun; Clarke, Edmund
12
2010
Automatic verification of sequential circuits using temporal logic. Zbl 0604.94011
Browne, Michael C.; Clarke, Edmund M.; Dill, David L.; Mishra, Bud
12
1986
Verifying concurrent message-passing C programs with recursive calls. Zbl 1180.68109
Chaki, S.; Clarke, E.; Kidd, N.; Reps, T.; Touili, T.
12
2006
The birth of model checking. Zbl 1142.68046
Clarke, Edmund M.
11
2008
State space reduction using partial order techniques. Zbl 1065.68506
Clarke, E. M.; Grumberg, O.; Minea, M.; Peled, D.
10
1999
The image computation problem in hybrid systems model checking. Zbl 1221.93118
Platzer, André; Clarke, Edmund M.
10
2007
Effective axiomatizations of Hoare logics. Zbl 0627.68010
Clarke, Edmund M. jun.; German, Steven M.; Halpern, Joseph Y.
10
1983
Automated assume-guarantee reasoning for simulation conformance. Zbl 1081.68612
Chaki, Sagar; Clarke, Edmund; Sinha, Nishant; Thati, Prasanna
10
2005
Environment abstraction for parameterized verification. Zbl 1176.68117
Clarke, Edmund; Talupur, Muralidhar; Veith, Helmut
9
2006
Handbook of model checking. Zbl 1390.68001
Clarke, Edmund M. (ed.); Henzinger, Thomas A. (ed.); Veith, Helmut (ed.); Bloem, Roderick (ed.)
9
2018
\(\delta \)-complete decision procedures for satisfiability over the reals. Zbl 1358.03028
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
8
2012
SAT based abstraction-refinement using ILP and machine learning techniques. Zbl 1010.68515
Clarke, Edmund; Gupta, Anubhav; Kukula, James; Strichman, Ofer
8
2002
Proving Ptolemy right: The environment abstraction framework for model checking concurrent systems. Zbl 1134.68403
Clarke, Edmund; Talupur, Murali; Veith, Helmut
8
2008
Efficient Craig interpolation for linear diophantine (dis)equations and linear modular equations. Zbl 1155.68439
Jain, Himanshu; Clarke, Edmund; Grumberg, Orna
8
2008
Solving QBF with counterexample guided refinement. Zbl 1351.68254
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
8
2016
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
Concurrent software verification with states, events, and deadlocks. Zbl 1103.68609
Chaki, Sagar; Clarke, Edmund; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant
7
2005
Reachability for linear hybrid automata using iterative relaxation abstraction. Zbl 1221.93115
Jha, Sumit K.; Krogh, Bruce H.; Weimer, James E.; Clarke, Edmund M.
7
2007
Hierarchical verification of asynchronous circuits using temporal logic. Zbl 0584.94022
Mishra, B.; Clarke, E.
7
1985
Analytica — an experiment in combining theorem proving and symbolic computation. Zbl 0916.68143
Bauer, Andrej; Clarke, Edmund; Zhao, Xudong
6
1998
Model checking. Zbl 1066.68075
Clarke, Edmund M.; Schlingloff, Bernd-Holger
6
2001
SAT-based compositional verification using lazy learning. Zbl 1135.68483
Sinha, Nishant; Clarke, Edmund
6
2007
SAT based predicate abstraction for hardware verification. Zbl 1204.68129
Clarke, Edmund; Talupur, Muralidhar; Veith, Helmut; Wang, Dong
6
2004
Program invariants as fixedpoints. Zbl 0399.68022
Clarke, E. M.
6
1979
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
Characterizing Kripke structures in temporal logic. Zbl 0626.03019
Browne, M. C.; Clarke, E. M.; Grümberg, O.
6
1987
Bayesian statistical model checking with application to Simulink/Stateflow verification. Zbl 1361.68154
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
6
2010
Bayesian statistical model checking with application to Stateflow/Simulink verification. Zbl 1291.68273
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
6
2013
Statistical model checking for cyber-physical systems. Zbl 1348.68128
Clarke, Edmund M.; Zuliani, Paolo
6
2011
Combining decision diagrams and SAT procedures for efficient symbolic model checking. Zbl 0974.68526
Williams, Poul F.; Biere, Armin; Clarke, Edmund M.; Gupta, Anubhav
5
2000
Refining abstractions of hybrid systems using counterexample fragments. Zbl 1078.93041
Fehnker, Ansgar; Clarke, Edmund; Jha, Sumit Kumar; Krogh, Bruce
5
2005
Computing differential invariants of hybrid systems as fixed points. Zbl 1180.93024
Platzer, André; Clarke, Edmund M.
5
2009
Arithmetic strengthening for shape analysis. Zbl 1211.68094
Magill, Stephen; Berdine, Josh; Clarke, Edmund; Cook, Byron
5
2007
Dynamic component substitutability analysis. Zbl 1120.68421
Sharygina, Natasha; Chaki, Sagar; Clarke, Edmund; Sinha, Nishant
5
2005
Design and synthesis of synchronization skeletons using branching time temporal logic. Zbl 1142.68431
Clarke, Edmund M.; Emerson, E. Allen
4
2008
Verification of evolving software via component substitutability analysis. Zbl 1147.68047
Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant
4
2008
Can message buffers be axiomatized in linear temporal logic? Zbl 0591.68022
Sistla, A. P.; Clarke, E. M.; Francez, N.; Meyer, A. R.
4
1984
Expressibility results for linear-time and branching-time logics. (Technical contribution). Zbl 0683.68030
Clarke, E. M.; Drăghicescu, I. A.
4
1989
A synthesis of two approaches for verifying finite state concurrent systems. Zbl 0688.68019
Clarke, E. M.; Grumberg, O.; Kurshan, R. P.
4
1989
Learning probabilistic systems from tree samples. Zbl 1362.68122
Komuravelli, Anvesh; Păsăreanu, Corina S.; Clarke, Edmund M.
4
2012
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.
3
1993
Synthesis of resource invariants for concurrent programs. Zbl 0468.68024
Clarke, Edmund Melson jun.
3
1980
Verification of SpecC using predicate abstraction. Zbl 1117.68046
Clarke, Edmund; Jain, Himanshu; Kroening, Daniel
3
2007
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
3
2005
Counterexamples revisited: principles, algorithms, applications. Zbl 1274.68179
Clarke, Edmund; Veith, Helmut
3
2003
On simulation-based probabilistic model checking of mixed-analog circuits. Zbl 1207.68205
Clarke, Edmund; Donzé, Alexandre; Legay, Axel
3
2010
Reasoning about procedures as parameters in the language L4. Zbl 0692.68011
German, Steven M.; Clarke, Edmund M.; Halpern, Joseph Y.
3
1989
\(\delta\)-decidability over the reals. Zbl 1364.03065
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
3
2012
Analysis and verification of real-time systems using quantitative symbolic algorithms. Zbl 1065.68505
Aguiar Campos, Sérgio Vale; Clarke, Edmund
2
1999
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
Making predicate abstraction efficient: how to eliminate redundant predicates. Zbl 1278.68163
Clarke, Edmund; Grumberg, Orna; Talupur, Muralidhar; Wang, Dong
2
2003
A synthesis of two approaches for verifying finite state concurrent systems. Zbl 0782.68078
Clarke, E. M.; Grumberg, O.; Kurshan, R. P.
2
1992
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
2
2015
Automatic verification of asynchronous circuits. Zbl 0541.94038
Clarke, E.; Mishra, B.
2
1984
The characterization problem for Hoare logics. With discussion by P. Aczel, J. V. Tucker and J. C. Shepherdson. Zbl 0598.68035
Clarke, E. M. jun.
2
1984
Rare-event verification for stochastic hybrid systems. Zbl 1362.68192
Zuliani, Paolo; Baier, Christel; Clarke, Edmund M.
2
2012
SMT-based analysis of virtually synchronous distributed hybrid systems. Zbl 1364.68258
Bae, Kyungmin; Ölveczky, Peter Csaba; Kong, Soonho; Gao, Sicun; Clarke, Edmund M.
2
2016
Computational modeling and verification of signaling pathways in cancer. Zbl 1349.92074
Gong, Haijun; Zuliani, Paolo; Komuravelli, Anvesh; Faeder, James R.; Clarke, Edmund M.
2
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
2
2003
Abstract BDDs: A technique for using abstraction in model checking. Zbl 0949.68105
Clarke, Edmund; Jha, Somesh; Lu, Yuan; Wang, Dong
1
1999
Partial order reductions for security protocol verification. Zbl 0965.68053
Clarke, Edmund; Jha, Somesh; Marrero, Will
1
2000
Model checking semi-continuous time model using BDDS. Zbl 0920.68076
Campos, Sergio; Teixeira, Marcio; Minea, Marius; Kuehlmann, Andreas; Clarke, Edmund
1
1999
Using combinatorial optimization methods for quantification scheduling. Zbl 1002.68512
Chauhan, P.; Clarke, E.; Jha, S.; Kukula, J.; Veith, H.; Wang, D.
1
2001
SAT-based counterexample guided abstraction refinement. Zbl 1077.68681
Clarke, Edmund M.
1
2002
Program compatibility approaches. Zbl 1196.68044
Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant
1
2006
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
Clarke, Edmund M. (ed.); Voronkov, Andrei (ed.)
1
2010
Model checking. 2nd expanded and updated edition. Zbl 1423.68002
Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut
15
2018
Handbook of model checking. Zbl 1390.68001
Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick
9
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
8
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.
2
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
2
2015
\(2^{5}\) years of model checking. Zbl 1434.68296
Clarke, Edmund M.; Wang, Qinsi
1
2015
dReal: an SMT solver for nonlinear theories over the reals. Zbl 1381.68268
Gao, Sicun; Kong, Soonho; Clarke, Edmund M.
17
2013
Bayesian statistical model checking with application to Stateflow/Simulink verification. Zbl 1291.68273
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
6
2013
Solving QBF with counterexample guided refinement. Zbl 1273.68178
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
20
2012
\(\delta \)-complete decision procedures for satisfiability over the reals. Zbl 1358.03028
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
8
2012
Learning probabilistic systems from tree samples. Zbl 1362.68122
Komuravelli, Anvesh; Păsăreanu, Corina S.; Clarke, Edmund M.
4
2012
\(\delta\)-decidability over the reals. Zbl 1364.03065
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
3
2012
Rare-event verification for stochastic hybrid systems. Zbl 1362.68192
Zuliani, Paolo; Baier, Christel; Clarke, Edmund M.
2
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.
2
2012
Statistical model checking for cyber-physical systems. Zbl 1348.68128
Clarke, Edmund M.; Zuliani, Paolo
6
2011
Statistical verification of probabilistic properties with unbounded until. Zbl 1325.68158
Younes, Håkan L. S.; Clarke, Edmund M.; Zuliani, Paolo
1
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
12
2010
Bayesian statistical model checking with application to Simulink/Stateflow verification. Zbl 1361.68154
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
6
2010
On simulation-based probabilistic model checking of mixed-analog circuits. Zbl 1207.68205
Clarke, Edmund; Donzé, Alexandre; Legay, Axel
3
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
Clarke, Edmund M.; Voronkov, Andrei
1
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
13
2009
Computing differential invariants of hybrid systems as fixed points. Zbl 1180.93024
Platzer, André; Clarke, Edmund M.
5
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
14
2008
Computing differential invariants of hybrid systems as fixedpoints. Zbl 1155.68445
Platzer, André; Clarke, Edmund M.
12
2008
The birth of model checking. Zbl 1142.68046
Clarke, Edmund M.
11
2008
Proving Ptolemy right: The environment abstraction framework for model checking concurrent systems. Zbl 1134.68403
Clarke, Edmund; Talupur, Murali; Veith, Helmut
8
2008
Efficient Craig interpolation for linear diophantine (dis)equations and linear modular equations. Zbl 1155.68439
Jain, Himanshu; Clarke, Edmund; Grumberg, Orna
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
Design and synthesis of synchronization skeletons using branching time temporal logic. Zbl 1142.68431
Clarke, Edmund M.; Emerson, E. Allen
4
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.
10
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.
7
2007
SAT-based compositional verification using lazy learning. Zbl 1135.68483
Sinha, Nishant; Clarke, Edmund
6
2007
Arithmetic strengthening for shape analysis. Zbl 1211.68094
Magill, Stephen; Berdine, Josh; Clarke, Edmund; Cook, Byron
5
2007
Verification of SpecC using predicate abstraction. Zbl 1117.68046
Clarke, Edmund; Jain, Himanshu; Kroening, Daniel
3
2007
Verifying concurrent message-passing C programs with recursive calls. Zbl 1180.68109
Chaki, S.; Clarke, E.; Kidd, N.; Reps, T.; Touili, T.
12
2006
Environment abstraction for parameterized verification. Zbl 1176.68117
Clarke, Edmund; Talupur, Muralidhar; Veith, Helmut
9
2006
Program compatibility approaches. Zbl 1196.68044
Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant
1
2006
SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
20
2005
Automated assume-guarantee reasoning for simulation conformance. Zbl 1081.68612
Chaki, Sagar; Clarke, Edmund; Sinha, Nishant; Thati, Prasanna
10
2005
Concurrent software verification with states, events, and deadlocks. Zbl 1103.68609
Chaki, Sagar; Clarke, Edmund; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant
7
2005
Refining abstractions of hybrid systems using counterexample fragments. Zbl 1078.93041
Fehnker, Ansgar; Clarke, Edmund; Jha, Sumit Kumar; Krogh, Bruce
5
2005
Dynamic component substitutability analysis. Zbl 1120.68421
Sharygina, Natasha; Chaki, Sagar; Clarke, Edmund; Sinha, Nishant
5
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
3
2005
A tool for checking ANSI-C programs. Zbl 1126.68470
Clarke, Edmund; Kroening, Daniel; Lerda, Flavio
56
2004
Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
13
2004
State/event-based software model checking. Zbl 1196.68129
Chaki, Sagar; Clarke, Edmund M.; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant
13
2004
Completeness and complexity of bounded model checking. Zbl 1202.68244
Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer
13
2004
Verification by network decomposition. Zbl 1099.68653
Clarke, Edmund; Talupur, Muralidhar; Touili, Tayssir; Veith, Helmut
12
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
73
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
20
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
12
2003
Counterexamples revisited: principles, algorithms, applications. Zbl 1274.68179
Clarke, Edmund; Veith, Helmut
3
2003
Making predicate abstraction efficient: how to eliminate redundant predicates. Zbl 1278.68163
Clarke, Edmund; Grumberg, Orna; Talupur, Muralidhar; Wang, Dong
2
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
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
78
2002
SAT based abstraction-refinement using ILP and machine learning techniques. Zbl 1010.68515
Clarke, Edmund; Gupta, Anubhav; Kukula, James; Strichman, Ofer
8
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
SAT-based counterexample guided abstraction refinement. Zbl 1077.68681
Clarke, Edmund M.
1
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
Bounded model checking using satisfiability solving. Zbl 0985.68038
Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan
47
2001
Model checking. Zbl 1066.68075
Clarke, Edmund M.; Schlingloff, Bernd-Holger
6
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
117
2000
NuSMV: A new symbolic model checker. Zbl 1059.68582
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco
32
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
5
2000
Partial order reductions for security protocol verification. Zbl 0965.68053
Clarke, Edmund; Jha, Somesh; Marrero, Will
1
2000
NuSMV: A new symbolic model verifier. Zbl 1046.68587
Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M.
34
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
23
1999
State space reduction using partial order techniques. Zbl 1065.68506
Clarke, E. M.; Grumberg, O.; Minea, M.; Peled, D.
10
1999
Analysis and verification of real-time systems using quantitative symbolic algorithms. Zbl 1065.68505
Aguiar Campos, Sérgio Vale; Clarke, Edmund
2
1999
Abstract BDDs: A technique for using abstraction in model checking. Zbl 0949.68105
Clarke, Edmund; Jha, Somesh; Lu, Yuan; Wang, Dong
1
1999
Model checking semi-continuous time model using BDDS. Zbl 0920.68076
Campos, Sergio; Teixeira, Marcio; Minea, Marius; Kuehlmann, Andreas; Clarke, Edmund
1
1999
Analytica — an experiment in combining theorem proving and symbolic computation. Zbl 0916.68143
Bauer, Andrej; Clarke, Edmund; Zhao, Xudong
6
1998
Symbolic model checking for probabilistic processes. Zbl 1401.68180
Baier, Christel; Clarke, Edmund M.; Hartonas-Garmhausen, Vasiliki; Kwiatkowska, Marta; Ryan, Mark
17
1997
An improved algorithm for the evaluation of fixpoint expressions. Zbl 0901.68118
Browne, A.; Clarke, E. M.; Jha, S.; Long, D. E.; Marrero, W.
16
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
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.
3
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.
148
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
Clarke, Edmund M.; Kurshan, Robert P.
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.
1
1990
Reasoning about networks with many identical finite state processes. Zbl 0709.68610
Browne, M. C.; Clarke, E. M.; Grumberg, O.
22
1989
Compositional model checking. Zbl 0716.68035
Clarke, E. M.; Long, D. E.; McMillan, K. L.
19
1989
Expressibility results for linear-time and branching-time logics. (Technical contribution). Zbl 0683.68030
Clarke, E. M.; Drăghicescu, I. A.
4
1989
A synthesis of two approaches for verifying finite state concurrent systems. Zbl 0688.68019
Clarke, E. M.; Grumberg, O.; Kurshan, R. P.
4
1989
Reasoning about procedures as parameters in the language L4. Zbl 0692.68011
German, Steven M.; Clarke, Edmund M.; Halpern, Joseph Y.
3
1989
Parthenon: A parallel theorem prover for non-Horn clauses. Zbl 0716.68076
Bose, Soumitra; Clarke, Edmund M.; Long, David E.; Michaylov, Spiro
1
1989
Characterizing finite Kripke structures in propositional temporal logic. Zbl 0677.03011
Browne, M. C.; Clarke, E. M.; Grümberg, O.
58
1988
Characterizing Kripke structures in temporal logic. Zbl 0626.03019
Browne, M. C.; Clarke, E. M.; Grümberg, O.
6
1987
Automatic verification of finite-state concurrent systems using temporal logic specifications. Zbl 0591.68027
Clarke, E. M.; Emerson, E. A.; Sistla, A. P.
247
1986
Automatic verification of sequential circuits using temporal logic. Zbl 0604.94011
Browne, Michael C.; Clarke, Edmund M.; Dill, David L.; Mishra, Bud
12
1986
...and 14 more Documents
all top 5

Cited by 2,208 Authors

27 Vardi, Moshe Y.
21 Kröning, Daniel
20 Kupferman, Orna
19 Clarke, Edmund Melson jun.
17 Duan, Zhenhua
16 Grumberg, Orna
15 Tian, Cong
14 Peled, Doron A.
13 Henzinger, Thomas A.
12 Baier, Christel
12 Cimatti, Alessandro
12 Zhang, Nan
11 Abdulla, Parosh Aziz
11 Lange, Martin
11 Pnueli, Amir
10 Demri, Stéphane P.
10 Kwiatkowska, Marta Z.
10 Murano, Aniello
10 Platzer, André
9 Biere, Armin
9 Katoen, Joost-Pieter
9 Laroussinie, François
9 Larsen, Kim Guldstrand
9 Markey, Nicolas
8 Brim, Luboš
8 Jamroga, Wojciech
8 Raskin, Jean-François
8 Reynolds, Mark Alexander
8 Sharygina, Natasha
8 Tonetta, Stefano
8 Veith, Helmut
8 Zhang, Lijun
7 Dasgupta, Pallab
7 Dixon, Clare
7 Emerson, Ernest Allen
7 Finkbeiner, Bernd
7 Gnesi, Stefania
7 Halpern, Joseph Yehuda
7 Konnov, Igor V.
7 McMillan, Kenneth L.
7 Roveri, Marco
7 Sifakis, Joseph
6 Bensalem, Saddek
6 Bouyer, Patricia
6 Fisman, Dana
6 Giacobazzi, Roberto
6 Gurfinkel, Arie
6 Hermanns, Holger
6 Jonsson, Bengt
6 Kesten, Yonit
6 Legay, Axel
6 Lomuscio, Alessio
6 Marques-Silva, João P.
6 Meseguer Guaita, José
6 Norman, Gethin
6 Penczek, Wojciech
6 Rümmer, Philipp
6 Schewe, Sven
6 Steffen, Bernhard
6 Strichman, Ofer
6 Touili, Tayssir
6 Wintersteiger, Christoph M.
6 Wooldridge, Michael J.
6 Zhan, Naijun
5 Barrett, Clark W.
5 Becker, Bernd
5 Beneš, Nikola
5 Bozzelli, Laura
5 Chaki, Sagar
5 Chakrabarti, Partha Pratim
5 Cleaveland, Rance
5 Cook, Byron
5 Dill, David L.
5 Fantechi, Alessandro
5 Griggio, Alberto
5 Gutierrez, Julian
5 Ipate, Florentin
5 Janota, Mikoláš
5 Järvisalo, Matti
5 Kulkarni, Sandeep S.
5 Majster-Cederbaum, Mila E.
5 Montanari, Angelo
5 Mundhenk, Martin
5 Olarte, Carlos
5 Ouaknine, Joel O.
5 Perelli, Giuseppe
5 Podelski, Andreas
5 Ranzato, Francesco
5 Ratschan, Stefan
5 Rossi, Matteo A. C.
5 Rybakov, Vladimir Vladimirovich
5 Sebastiani, Roberto
5 Smolka, Scott A.
5 Valmari, Antti
5 Wahl, Thomas
5 Widder, Josef
5 Wolter, Frank
4 Abate, Alessandro
4 Ábrahám, Erika
4 Angluin, Dana
...and 2,108 more Authors
all top 5

Cited in 119 Serials

166 Theoretical Computer Science
121 Formal Methods in System Design
79 Information and Computation
69 Formal Aspects of Computing
39 Acta Informatica
39 Journal of Automated Reasoning
36 Artificial Intelligence
27 Journal of Computer and System Sciences
26 Information Processing Letters
26 The Journal of Logic and Algebraic Programming
23 Science of Computer Programming
16 Journal of Applied Logic
16 Journal of Logical and Algebraic Methods in Programming
15 International Journal of Foundations of Computer Science
15 Annals of Mathematics and Artificial Intelligence
11 Annals of Pure and Applied Logic
11 Discrete Event Dynamic Systems
11 Distributed Computing
11 ACM Transactions on Computational Logic
10 Journal of Computer Science and Technology
10 Logical Methods in Computer Science
9 Journal of Symbolic Computation
8 Automatica
8 MSCS. Mathematical Structures in Computer Science
8 Journal of Applied Non-Classical Logics
8 Journal of Applied Mathematics
7 Programming and Computer Software
7 European Journal of Control
7 Theory of Computing Systems
6 Studia Logica
6 Journal of Logic, Language and Information
5 Discrete Applied Mathematics
5 Information Sciences
5 Fundamenta Informaticae
5 Nonlinear Analysis. Hybrid Systems
4 Real-Time Systems
4 The Bulletin of Symbolic Logic
4 RAIRO. Theoretical Informatics and Applications
4 Sādhanā
4 Computer Languages, Systems & Structures
4 Science China. Information Sciences
3 Synthese
3 Algorithmica
3 Constraints
3 International Journal of Applied Mathematics and Computer Science
3 Theory and Practice of Logic Programming
3 Frontiers of Computer Science
3 Computer Science Review
2 International Journal of General Systems
2 BIT
2 The Journal of Symbolic Logic
2 Notre Dame Journal of Formal Logic
2 International Journal of Parallel Programming
2 International Journal of Approximate Reasoning
2 Journal of Parallel and Distributed Computing
2 JETAI. Journal of Experimental & Theoretical Artificial Intelligence
2 Automation and Remote Control
2 Cybernetics and Systems Analysis
2 Journal of Combinatorial Optimization
2 Journal of the ACM
2 Science in China. Series F
1 ACM Computing Surveys
1 Computers & Mathematics with Applications
1 Discrete Mathematics
1 International Journal of Control
1 International Journal of Theoretical Physics
1 Calcolo
1 Computing
1 Fuzzy Sets and Systems
1 Journal of Mathematical Economics
1 Journal of Philosophical Logic
1 Journal of Soviet Mathematics
1 Nonlinear Analysis. Theory, Methods & Applications. Series A: Theory and Methods
1 RAIRO, Informatique Théorique
1 SIAM Journal on Computing
1 Siberian Mathematical Journal
1 Cybernetics
1 Systems & Control Letters
1 International Journal of Production Research
1 Order
1 New Generation Computing
1 Computers & Operations Research
1 Mathematical and Computer Modelling
1 Machine Learning
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
1 International Journal of Bifurcation and Chaos in Applied Sciences and Engineering
1 Archives of Control Sciences
1 Applied Categorical Structures
1 Journal of Mathematical Sciences (New York)
1 Computational & Mathematical Organization Theory
1 INFORMS Journal on Computing
1 Mathematical Problems in Engineering
1 Journal of Applied Mathematics and Decision Sciences
1 Chaos
...and 19 more Serials

Citations by Year

Wikidata Timeline

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