×

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, E.; Clarke, E. M.; Clarke, E. M. jun.; Clarke, Edmund; Clarke, Edmund M.; Clarke, Edmund M. jun.; Clarke, Edmund Melson; Clarke, Edmund Melson jun.
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, Anca
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.
...and 22 more Co-Authors

Publications by Year

Citations contained in zbMATH

115 Publications have been cited 2,183 times in 1,445 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.
248
1986
Model checking. Zbl 0847.68063
Clarke, E.; Grumberg, O.; Long, D.
238
1996
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.
153
1992
Counterexample-guided abstraction refinement. Zbl 0974.68517
Clarke, Edmund; Grumberg, Orna; Jha, Somesh; Lu, Yuan; Veith, Helmut
119
2000
Design and synthesis of synchronization skeletons using branching time temporal logic. Zbl 0546.68014
Clarke, Edmund M.; Emerson, E. Allen
93
1982
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
72
2003
Using branching time temporal logic to synthesize synchronization skeletons. Zbl 0514.68032
Emerson, E. Allen; Clarke, Edmund M.
66
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
55
2004
Bounded model checking using satisfiability solving. Zbl 0985.68038
Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan
46
2001
Characterizing correctness properties of parallel programs using fixpoints. Zbl 0456.68016
Emerson, E. Allen; Clarke, Edmund M.
36
1980
NuSMV: A new symbolic model checker. Zbl 1059.68582
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco
34
2000
NuSMV: A new symbolic model verifier. Zbl 1046.68587
Cimatti, A.; Clarke, E.; Giunchiglia, F.; Roveri, M.
34
1999
Programming language constructs for which it is impossible to obtain good Hoare axiom systems. Zbl 0388.68008
Clarke, Edmund Melson jun.
29
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
28
1999
Reasoning about networks with many identical finite state processes. Zbl 0709.68610
Browne, M. C.; Clarke, E. M.; Grumberg, O.
23
1989
Solving QBF with counterexample guided refinement. Zbl 1273.68178
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
20
2012
SATABS: SAT-based predicate abstraction for ANSI-C. Zbl 1087.68586
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
20
2005
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
Compositional model checking. Zbl 0716.68035
Clarke, E. M.; Long, D. E.; McMillan, K. L.
19
1989
An improved algorithm for the evaluation of fixpoint expressions. Zbl 0901.68118
Browne, A.; Clarke, E. M.; Jha, S.; Long, D. E.; Marrero, W.
18
1997
dReal: an SMT solver for nonlinear theories over the reals. Zbl 1381.68268
Gao, Sicun; Kong, Soonho; Clarke, Edmund M.
17
2013
Symbolic model checking for probabilistic processes. Zbl 1401.68180
Baier, Christel; Clarke, Edmund M.; Hartonas-Garmhausen, Vasiliki; Kwiatkowska, Marta; Ryan, Mark
17
1997
Model checking. 2nd expanded and updated edition. Zbl 1423.68002
Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut
13
2018
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
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
13
2008
Completeness and complexity of bounded model checking. Zbl 1202.68244
Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer
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
Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
13
2004
Computing differential invariants of hybrid systems as fixedpoints. Zbl 1155.68445
Platzer, André; Clarke, Edmund M.
12
2008
Verifying concurrent message-passing C programs with recursive calls. Zbl 1180.68109
Chaki, S.; Clarke, E.; Kidd, N.; Reps, T.; Touili, T.
12
2006
Verification by network decomposition. Zbl 1099.68653
Clarke, Edmund; Talupur, Muralidhar; Touili, Tayssir; Veith, Helmut
12
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
Automatic verification of sequential circuits using temporal logic. Zbl 0604.94011
Browne, Michael C.; Clarke, Edmund M.; Dill, David L.; Mishra, Bud
12
1986
A non-prenex, non-clausal QBF solver with game-state learning. Zbl 1306.68161
Klieber, William; Sapra, Samir; Gao, Sicun; Clarke, Edmund
11
2010
The image computation problem in hybrid systems model checking. Zbl 1221.93118
Platzer, André; Clarke, Edmund M.
11
2007
Effective axiomatizations of Hoare logics. Zbl 0627.68010
Clarke, Edmund M. jun.; German, Steven M.; Halpern, Joseph Y.
11
1983
The birth of model checking. Zbl 1142.68046
Clarke, Edmund M.
10
2008
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
State space reduction using partial order techniques. Zbl 1065.68506
Clarke, E. M.; Grumberg, O.; Minea, M.; Peled, D.
9
1999
Solving QBF with counterexample guided refinement. Zbl 1351.68254
Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund
8
2016
Efficient Craig interpolation for linear diophantine (dis)equations and linear modular equations. Zbl 1155.68439
Jain, Himanshu; Clarke, Edmund; Grumberg, Orna
8
2008
Proving Ptolemy right: The environment abstraction framework for model checking concurrent systems. Zbl 1134.68403
Clarke, Edmund; Talupur, Murali; Veith, Helmut
8
2008
SAT based abstraction-refinement using ILP and machine learning techniques. Zbl 1010.68515
Clarke, Edmund; Gupta, Anubhav; Kukula, James; Strichman, Ofer
8
2002
Bayesian statistical model checking with application to Stateflow/Simulink verification. Zbl 1291.68273
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
7
2013
\(\delta \)-complete decision procedures for satisfiability over the reals. Zbl 1358.03028
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
7
2012
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
Concurrent software verification with states, events, and deadlocks. Zbl 1103.68609
Chaki, Sagar; Clarke, Edmund; Ouaknine, Joël; Sharygina, Natasha; Sinha, Nishant
7
2005
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
Hierarchical verification of asynchronous circuits using temporal logic. Zbl 0584.94022
Mishra, B.; Clarke, E.
7
1985
Handbook of model checking. Zbl 1390.68001
Clarke, Edmund M. (ed.); Henzinger, Thomas A. (ed.); Veith, Helmut (ed.); Bloem, Roderick (ed.)
6
2018
Statistical model checking for cyber-physical systems. Zbl 1348.68128
Clarke, Edmund M.; Zuliani, Paolo
6
2011
Bayesian statistical model checking with application to Simulink/Stateflow verification. Zbl 1361.68154
Zuliani, Paolo; Platzer, André; Clarke, Edmund M.
6
2010
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
6
2008
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
Model checking. Zbl 1066.68075
Clarke, Edmund M.; Schlingloff, Bernd-Holger
6
2001
Analytica — an experiment in combining theorem proving and symbolic computation. Zbl 0916.68143
Bauer, Andrej; Clarke, Edmund; Zhao, Xudong
6
1998
Characterizing Kripke structures in temporal logic. Zbl 0626.03019
Browne, M. C.; Clarke, E. M.; Grümberg, O.
6
1987
Program invariants as fixedpoints. Zbl 0399.68022
Clarke, E. M.
6
1979
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
Refining abstractions of hybrid systems using counterexample fragments. Zbl 1078.93041
Fehnker, Ansgar; Clarke, Edmund; Jha, Sumit Kumar; Krogh, Bruce
5
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
5
2000
Learning probabilistic systems from tree samples. Zbl 1362.68122
Komuravelli, Anvesh; Păsăreanu, Corina S.; Clarke, Edmund M.
4
2012
Verification of evolving software via component substitutability analysis. Zbl 1147.68047
Chaki, Sagar; Clarke, Edmund; Sharygina, Natasha; Sinha, Nishant
4
2008
Verification of SpecC using predicate abstraction. Zbl 1117.68046
Clarke, Edmund; Jain, Himanshu; Kroening, Daniel
4
2007
A synthesis of two approaches for verifying finite state concurrent systems. Zbl 0688.68019
Clarke, E. M.; Grumberg, O.; Kurshan, R. P.
4
1989
Expressibility results for linear-time and branching-time logics. (Technical contribution). Zbl 0683.68030
Clarke, E. M.; Drăghicescu, I. A.
4
1989
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
\(\delta\)-decidability over the reals. Zbl 1364.03065
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
3
2012
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
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
Reasoning about procedures as parameters in the language L4. Zbl 0692.68011
German, Steven M.; Clarke, Edmund M.; Halpern, Joseph Y.
3
1989
Synthesis of resource invariants for concurrent programs. Zbl 0468.68024
Clarke, Edmund Melson jun.
3
1980
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
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
On simulation-based probabilistic model checking of mixed-analog circuits. Zbl 1207.68205
Clarke, Edmund; Donzé, Alexandre; Legay, Axel
2
2010
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
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
Making predicate abstraction efficient: how to eliminate redundant predicates. Zbl 1278.68163
Clarke, Edmund; Grumberg, Orna; Talupur, Muralidhar; Wang, Dong
2
2003
Using combinatorial optimization methods for quantification scheduling. Zbl 1002.68512
Chauhan, P.; Clarke, E.; Jha, S.; Kukula, J.; Veith, H.; Wang, D.
2
2001
Partial order reductions for security protocol verification. Zbl 0965.68053
Clarke, Edmund; Jha, Somesh; Marrero, Will
2
2000
Analysis and verification of real-time systems using quantitative symbolic algorithms. Zbl 1065.68505
Aguiar Campos, Sérgio Vale; Clarke, Edmund
2
1999
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 0716.68076
Bose, Soumitra; Clarke, Edmund M.; Long, David E.; Michaylov, Spiro
2
1989
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
Automatic verification of asynchronous circuits. Zbl 0541.94038
Clarke, E.; Mishra, B.
2
1984
Reasoning about procedures as parameters. Zbl 0539.68010
German, S. M.; Clarke, E. M. jun.; Halpern, J. Y.
2
1984
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
\(2^{5}\) years of model checking. Zbl 1434.68296
Clarke, Edmund M.; Wang, Qinsi
1
2015
Quantifier elimination over finite fields using Gröbner bases. Zbl 1339.68321
Gao, Sicun; Platzer, André; Clarke, Edmund M.
1
2011
Model checking. 2nd expanded and updated edition. Zbl 1423.68002
Clarke, Edmund M. jun.; Grumberg, Orna; Kroening, Daniel; Peled, Doron; Veith, Helmut
13
2018
Handbook of model checking. Zbl 1390.68001
Clarke, Edmund M. (ed.); Henzinger, Thomas A. (ed.); Veith, Helmut (ed.); Bloem, Roderick (ed.)
6
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.
7
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.
7
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
Quantifier elimination over finite fields using Gröbner bases. Zbl 1339.68321
Gao, Sicun; Platzer, André; Clarke, Edmund M.
1
2011
Statistical verification of probabilistic properties with unbounded until. Zbl 1325.68158
Younes, Håkan L. S.; Clarke, Edmund M.; Zuliani, Paolo
1
2011
A non-prenex, non-clausal QBF solver with game-state learning. Zbl 1306.68161
Klieber, William; Sapra, Samir; Gao, Sicun; Clarke, Edmund
11
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
2
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. (ed.); Voronkov, Andrei (ed.)
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
13
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.
10
2008
Efficient Craig interpolation for linear diophantine (dis)equations and linear modular equations. Zbl 1155.68439
Jain, Himanshu; Clarke, Edmund; Grumberg, Orna
8
2008
Proving Ptolemy right: The environment abstraction framework for model checking concurrent systems. Zbl 1134.68403
Clarke, Edmund; Talupur, Murali; Veith, Helmut
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
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.
11
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
4
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
Dynamic component substitutability analysis. Zbl 1120.68421
Sharygina, Natasha; Chaki, Sagar; Clarke, Edmund; Sinha, Nishant
5
2005
Refining abstractions of hybrid systems using counterexample fragments. Zbl 1078.93041
Fehnker, Ansgar; Clarke, Edmund; Jha, Sumit Kumar; Krogh, Bruce
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
55
2004
Completeness and complexity of bounded model checking. Zbl 1202.68244
Clarke, Edmund; Kroening, Daniel; Ouaknine, Joël; Strichman, Ofer
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
Predicate abstraction of ANSI-C programs using SAT. Zbl 1090.68022
Clarke, Edmund; Kroening, Daniel; Sharygina, Natasha; Yorav, Karen
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
72
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
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
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
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
46
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.
2
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
119
2000
NuSMV: A new symbolic model checker. Zbl 1059.68582
Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco
34
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
2
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
28
1999
State space reduction using partial order techniques. Zbl 1065.68506
Clarke, E. M.; Grumberg, O.; Minea, M.; Peled, D.
9
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
On the semantic foundations of probabilistic synchronous reactive programs. Zbl 0943.68107
Baier, Christel; Clarke, Edmund M.; Hartonas-Garmhausen, Vasiliki
1
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.
18
1997
Symbolic model checking for probabilistic processes. Zbl 1401.68180
Baier, Christel; Clarke, Edmund M.; Hartonas-Garmhausen, Vasiliki; Kwiatkowska, Marta; Ryan, Mark
17
1997
Model checking. Zbl 0847.68063
Clarke, E.; Grumberg, O.; Long, D.
238
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.
153
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. (ed.); Kurshan, Robert P. (ed.)
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.
23
1989
Compositional model checking. Zbl 0716.68035
Clarke, E. M.; Long, D. E.; McMillan, K. L.
19
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
Expressibility results for linear-time and branching-time logics. (Technical contribution). Zbl 0683.68030
Clarke, E. M.; Drăghicescu, I. A.
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
2
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.
248
1986
...and 15 more Documents
all top 5

Cited by 2,403 Authors

27 Vardi, Moshe Y.
21 Kupferman, Orna
19 Clarke, Edmund Melson jun.
19 Kröning, Daniel
18 Duan, Zhenhua
18 Grumberg, Orna
16 Tian, Cong
15 Peled, Doron A.
14 Henzinger, Thomas A.
13 Baier, Christel
13 Pnueli, Amir
13 Zhang, Nan
11 Abdulla, Parosh Aziz
11 Cimatti, Alessandro
11 Lange, Martin
11 Murano, Aniello
10 Demri, Stéphane P.
10 Katoen, Joost-Pieter
10 Kwiatkowska, Marta Z.
10 Laroussinie, François
10 Platzer, André
9 Biere, Armin
9 Dixon, Clare
9 Larsen, Kim Guldstrand
9 Lomuscio, Alessio
9 Markey, Nicolas
9 Meseguer Guaita, José
8 Bouyer, Patricia
8 Brim, Luboš
8 Halpern, Joseph Yehuda
8 Jamroga, Wojciech
8 Sharygina, Natasha
8 Tonetta, Stefano
8 Touili, Tayssir
8 Veith, Helmut
8 Wooldridge, Michael J.
8 Zhang, Lijun
7 Bensalem, Saddek
7 Dasgupta, Pallab
7 Emerson, Ernest Allen
7 Finkbeiner, Bernd
7 Girard, Antoine
7 Gnesi, Stefania
7 Jonsson, Bengt
7 Konnov, Igor V.
7 McMillan, Kenneth L.
7 Norman, Gethin
7 Pappas, George J.
7 Penczek, Wojciech
7 Raskin, Jean-François
7 Reynolds, Mark Alexander
7 Roveri, Marco
7 Schewe, Sven
7 Sifakis, Joseph
7 Tahar, Sofiène
6 Beneš, Nikola
6 Giacobazzi, Roberto
6 Gurfinkel, Arie
6 Gutierrez, Julian
6 Hasan, Osman
6 Hermanns, Holger
6 Kesten, Yonit
6 Legay, Axel
6 Marques-Silva, João P.
6 Piazza, Carla
6 Rümmer, Philipp
6 Santone, Antonella
6 Shoham, Sharon
6 Steffen, Bernhard
6 Strichman, Ofer
6 Wintersteiger, Christoph M.
6 Zhan, Naijun
5 Abate, Alessandro
5 Barrett, Clark W.
5 Becker, Bernd
5 Bloem, Roderick
5 Bollig, Benedikt
5 Bozzelli, Laura
5 Chaki, Sagar
5 Chakrabarti, Partha Pratim
5 Cleaveland, Rance
5 Cook, Byron
5 Dill, David L.
5 Donaldson, Alastair F.
5 Fantechi, Alessandro
5 Fisman, Dana
5 Griggio, Alberto
5 Ipate, Florentin
5 Janota, Mikoláš
5 Järvisalo, Matti
5 Jobstmann, Barbara
5 Kamide, Norihiro
5 Konur, Savas
5 Kulkarni, Sandeep S.
5 Leucker, Martin
5 Majster-Cederbaum, Mila E.
5 Majumdar, Rupak
5 Mogavero, Fabio
5 Montanari, Angelo
5 Mundhenk, Martin
...and 2,303 more Authors
all top 5

Cited in 121 Serials

203 Theoretical Computer Science
121 Formal Methods in System Design
95 Information and Computation
67 Formal Aspects of Computing
49 Artificial Intelligence
39 Journal of Computer and System Sciences
37 Acta Informatica
37 Journal of Automated Reasoning
33 Information Processing Letters
33 The Journal of Logic and Algebraic Programming
27 Journal of Applied Logic
24 Science of Computer Programming
18 Journal of Logical and Algebraic Methods in Programming
15 Annals of Pure and Applied Logic
15 International Journal of Foundations of Computer Science
15 Annals of Mathematics and Artificial Intelligence
13 Automatica
11 Discrete Event Dynamic Systems
11 Distributed Computing
11 ACM Transactions on Computational Logic
10 Journal of Symbolic Computation
10 Journal of Computer Science and Technology
10 Logical Methods in Computer Science
10 Nonlinear Analysis. Hybrid Systems
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 Information Sciences
6 Studia Logica
6 Journal of Logic, Language and Information
5 Discrete Applied Mathematics
5 Computer Languages, Systems & Structures
4 Real-Time Systems
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 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 Fuzzy Sets and Systems
2 The Journal of Symbolic Logic
2 Notre Dame Journal of Formal Logic
2 Systems & Control Letters
2 International Journal of Parallel Programming
2 International Journal of Approximate Reasoning
2 Mathematical and Computer Modelling
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 Abstract and Applied 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 Applied Mathematics and Computation
1 Calcolo
1 Computing
1 Journal of Mathematical Economics
1 Journal of Philosophical Logic
1 Journal of Soviet Mathematics
1 Mathematics and Computers in Simulation
1 Nonlinear Analysis. Theory, Methods & Applications. Series A: Theory and Methods
1 RAIRO, Informatique Théorique
1 SIAM Journal on Computing
1 Cybernetics
1 International Journal of Production Research
1 Order
1 New Generation Computing
1 Computers & Operations Research
1 Machine Learning
1 Games and Economic Behavior
1 Linear Algebra and its Applications
1 Pattern Recognition
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
...and 21 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.