☰

Edmund M. Clarke - Publications

Affiliations: 
1982-2015 Computer Science Carnegie Mellon University, Pittsburgh, PA 
Website:
https://www.cs.cmu.edu/~emc/bio.html
Tree Info Similar researchers PubMed Report error

67 high-probability publications. We are testing a new system for linking publications to authors. You can help! If you notice any inaccuracies, please sign in and mark papers as correct or incorrect matches. If you identify any major omissions or other inaccuracies in the publication list, please let us know.

Year Citation  Score
2016 Janota M, Klieber W, Marques-Silva J, Clarke E. Solving QBF with counterexample guided refinement Artificial Intelligence. 234: 1-25. DOI: 10.1016/J.Artint.2016.01.004  0.359
2013 Zuliani P, Platzer A, Clarke EM. Bayesian statistical model checking with application to Stateflow/Simulink verification Formal Methods in System Design. 43: 338-367. DOI: 10.1007/s10703-013-0195-3  0.302
2010 Zuliani P, Platzer A, Clarke EM. Bayesian statistical model checking with application to simulink/stateflow verification Hscc'10 - Proceedings of the 13th Acm International Conference On Hybrid Systems: Computation and Control. 243-252. DOI: 10.1145/1755952.1755987  0.308
2010 Clarke EM, Kurshan RP, Veith H. The localization reduction and counterexample-guided abstraction refinement Lecture Notes in Computer Science. 6200: 61-71. DOI: 10.1007/978-3-642-13754-9_4  0.413
2009 Clarke EM, Emerson EA, Sifakis J. Model checking: Algorithmic verification and debugging Communications of the Acm. 52: 74-84. DOI: 10.1145/1592761.1592781  0.619
2009 Mathur A, Fujita M, Clarke E, Urard P. Functional Equivalence Verification Tools in High-Level Synthesis Flows Ieee Design & Test of Computers. 26: 88-95. DOI: 10.1109/Mdt.2009.79  0.383
2009 Jha SK, Clarke EM, Langmead CJ, Legay A, Platzer A, Zuliani P. A bayesian approach to model checking biological systems Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 5688: 218-234. DOI: 10.1007/978-3-642-03845-7_15  0.307
2008 Jain H, Kroening D, Sharygina N, Clarke EM. Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 27: 366-379. DOI: 10.1109/Tcad.2007.907270  0.439
2008 Lerda F, Kapinski J, Maka H, Clarke EM, Krogh BH. Model checking in-the-loop: Finding counterexamples by systematic simulation Proceedings of the American Control Conference. 2734-2740. DOI: 10.1109/ACC.2008.4586906  0.306
2005 Chaki S, Clarke E, Jha S, Veith H. An Iterative Framework for Simulation Conformance Journal of Logic and Computation. 15: 465-488. DOI: 10.1093/Logcom/Exi028  0.591
2005 Clarke E, Kroening D, Ouaknine J, Strichman O. Computational challenges in bounded model checking International Journal On Software Tools For Technology Transfer. 7: 174-183. DOI: 10.1007/S10009-004-0182-5  0.318
2005 Chaki S, Clarke E, Ouaknine J, Sharygina N, Sinha N. Concurrent software verification with states, events, and deadlocks Formal Aspects of Computing. 17: 461-483. DOI: 10.1007/s00165-005-0071-z  0.395
2004 Chaki S, Clarke EM, Groce A, Jha S, Veith H. Modular verification of software components in C Ieee Transactions On Software Engineering. 30: 388-402. DOI: 10.1109/Tse.2004.22  0.734
2004 Clarke EM, Gupta A, Strichman O. SAT-based counterexample-guided abstraction refinement Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 23: 1113-1123. DOI: 10.1109/Tcad.2004.829807  0.428
2004 Mota E, Clarke EM, Groce A, Oliveira W, Falcão M, Kanda J. VeriAgent: an Approach to Integrating UML and Formal Verification Tools Electronic Notes in Theoretical Computer Science. 95: 111-129. DOI: 10.1016/J.Entcs.2004.04.008  0.698
2003 Clarke E, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-guided abstraction refinement for symbolic model checking Journal of the Acm (Jacm). 50: 752-794. DOI: 10.1145/876638.876643  0.63
2003 Clarke EM, Fehnker A, Han Z, Krogh BH, Ouaknine J, Stursberg O, Theobald M. Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems International Journal of Foundations of Computer Science. 14: 583-604. DOI: 10.1142/S012905410300190X  0.436
2003 Chaki S, Ouaknine J, Yorav K, Clarke EM. Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach Electronic Notes in Theoretical Computer Science. 89: 417-432. DOI: 10.1016/S1571-0661(05)80004-0  0.453
2003 Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y. Bounded Model Checking Advances in Computers. 58: 117-148. DOI: 10.1016/S0065-2458(03)58003-2  0.459
2003 Clarke EM, Veith H. Counterexamples Revisited: Principles, Algorithms, Applications Lecture Notes in Computer Science. 208-224. DOI: 10.1007/978-3-540-39910-0_9  0.384
2003 Chaki S, Clarke EM, Groce A, Strichman O. Predicate Abstraction with Minimum Predicates. Lecture Notes in Computer Science. 19-34. DOI: 10.1007/978-3-540-39724-3_5  0.702
2002 Clarke EM, Fujita M, Rajan SP, Reps TW, Shankar S, Teitelbaum T. Program slicing for VHDL International Journal On Software Tools For Technology Transfer. 4: 125-137. DOI: 10.1007/S100090100069  0.439
2001 Campos S, Teixeira M, Minea M, Kuehlmann A, Clarke E. Model checking semi-continuous time models using BDDs Electronic Notes in Theoretical Computer Science. 23: 79-91. DOI: 10.1016/S1571-0661(04)80670-4  0.42
2001 Biere A, Clarke EM, Zhu Y. Combining Local and Global Model Checking Electronic Notes in Theoretical Computer Science. 23: 34-45. DOI: 10.1016/S1571-0661(04)80667-4  0.404
2001 Campos SVA, Clarke E. The Verus language: representing time efficiently with BDDs Theoretical Computer Science. 253: 95-118. DOI: 10.1016/S0304-3975(00)00090-6  0.446
2001 Chauhan P, Clarke EM, Jha S, Kukula JH, Veith H, Wang D. Using Combinatorial Optimization Methods for Quantification Scheduling Lecture Notes in Computer Science. 293-309. DOI: 10.1007/3-540-44798-9_24  0.553
2001 Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Progress on the State Explosion Problem in Model Checking Lecture Notes in Computer Science. 176-194. DOI: 10.1007/3-540-44577-3_12  0.593
2000 Clarke EM, Jha S, Marrero W. Verifying security protocols with Brutus Acm Transactions On Software Engineering and Methodology. 9: 443-487. DOI: 10.1145/363516.363528  0.534
2000 Clarke EM. Automatic verification of hardware and software systems Acm Sigsoft Software Engineering Notes. 25: 41-42. DOI: 10.1145/340855.340875  0.368
2000 Hartonas-Garmhausen V, Campos S, Cimatti A, Clarke E, Giunchiglia F. Verification of a safety-critical railway interlocking system with real-time constraints Science of Computer Programming. 36: 53-64. DOI: 10.1016/S0167-6423(99)00016-7  0.42
2000 Cimatti A, Clarke EM, Giunchiglia F, Roveri M. NUSMV: a new symbolic model checker International Journal On Software Tools For Technology Transfer. 2: 410-425. DOI: 10.1007/S100090050046  0.383
1999 Baier C, Clarke EM, Hartonas-Garmhausen V. On the Semantic Foundations of Probabilistic Synchronous Reactive Programs Electronic Notes in Theoretical Computer Science. 22: 3-28. DOI: 10.1016/S1571-0661(05)80594-8  0.4
1999 Clarke EM, Grumberg O, Minea M, Peled D. State space reduction using partial order techniques International Journal On Software Tools For Technology Transfer. 2: 279-287. DOI: 10.1007/S100090050035  0.379
1999 Campos SVA, Clarke EM. Analysis and verification of real-time systems using quantitative symbolic algorithms International Journal On Software Tools For Technology Transfer. 2: 260-269. DOI: 10.1007/S100090050033  0.417
1999 Clarke EM, Fujita M, Rajan SP, Reps TW, Shankar S, Teitelbaum T. Program Slicing of Hardware Description Languages Lecture Notes in Computer Science. 298-312. DOI: 10.1007/3-540-48153-2_22  0.389
1999 Clarke EM, Jha S, Lu Y, Wang D. Abstract BDDs: A Technque for Using Abstraction in Model Checking Lecture Notes in Computer Science. 172-186. DOI: 10.1007/3-540-48153-2_14  0.578
1998 Bauer A, Clarke E, Zhao X. Analytica – An Experiment in Combining Theorem Proving and Symbolic Computation Journal of Automated Reasoning. 21: 295-325. DOI: 10.1023/A:1006079212546  0.357
1997 Clarke EM, Grumberg O, Jha S. Verifying parameterized networks Acm Transactions On Programming Languages and Systems. 19: 726-750. DOI: 10.1145/265943.265960  0.543
1997 Browne A, Clarke EM, Jha S, Long DE, Marrero W. An improved algorithm for the evaluation of fixpoint expressions Theoretical Computer Science. 178: 237-255. DOI: 10.1016/S0304-3975(96)00228-9  0.357
1997 Campos S, Clarke EM, Minea M. Symbolic techniques for formally verifying industrial systems Science of Computer Programming. 29: 79-98. DOI: 10.1016/S0167-6423(96)00030-5  0.456
1997 Campos S, Clarke E. The verus language: Representing time efficiently with BDDs Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). 1231: 64-78. DOI: 10.1007/3-540-63010-4_5  0.344
1996 Clarke EM, Wing JM. Formal methods: state of the art and future directions Acm Computing Surveys. 28: 626-643. DOI: 10.1145/242223.242257  0.448
1995 Campos S, Clarke E, Marrero W, Minea M. Verus Acm Sigplan Notices. 30: 70-78. DOI: 10.1145/216633.216661  0.355
1994 Clarke EM, Grumberg O, Long DE. Model checking and abstraction Acm Transactions On Programming Languages and Systems. 16: 1512-1542. DOI: 10.1145/186025.186051  0.455
1994 Burch JR, Clarke EM, Long DE, McMillan KL, Dill DL. Symbolic Model Checking for Sequential Circuit Verification Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 13: 401-424. DOI: 10.1109/43.275352  0.627
1993 Clarke EM, Draghicescu IA, Kurshan RP. A unified approach for showing language inclusion and equivalence between various types of Ω-automata Information Processing Letters. 46: 301-308. DOI: 10.1016/0020-0190(93)90069-L  0.392
1993 Anger FD, Clarke EM. New and used temporal models: An issue of time Applied Intelligence. 3: 5-15. DOI: 10.1007/Bf00871719  0.346
1992 Clarke EM, Grumberg O, Kurshan RP. A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems Journal of Logic and Computation. 2: 605-618. DOI: 10.1093/Logcom/2.5.605  0.334
1992 Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ. Symbolic model checking: 1020 States and beyond Information and Computation. 98: 142-170. DOI: 10.1016/0890-5401(92)90017-A  0.345
1992 Bose S, Clarke EM, Long DE, Michaylov S. Parthenon: a parallel theorem prover for non-Horn clauses Journal of Automated Reasoning. 8: 153-181. DOI: 10.1007/Bf00244281  0.413
1992 Moon I, Powers GJ, Burch JR, Clarke EM. Automatic verification of sequential control systems using temporal logic Aiche Journal. 38: 67-75. DOI: 10.1002/Aic.690380107  0.369
1989 German SM, Clarke EM, Halpern JY. Reasoning about procedures as parameters in the language L4 Information & Computation. 83: 265-359. DOI: 10.1016/0890-5401(89)90040-0  0.367
1988 Clarke EM, Feng Y. Escher-a geometrical layout system for recursively defined circuits Ieee Transactions On Computer-Aided Design of Integrated Circuits and Systems. 7: 908-918. DOI: 10.1109/43.3222  0.341
1988 Browne MC, Clarke EM, Grümberg O. Characterizing finite Kripke structures in propositional temporal logic Theoretical Computer Science. 59: 115-131. DOI: 10.1016/0304-3975(88)90098-9  0.339
1986 Clarke EM, Emerson EA, Sistla AP. Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications Acm Transactions On Programming Languages and Systems (Toplas). 8: 244-263. DOI: 10.1145/5397.5399  0.582
1986 Anantharaman TS, Clarke EM, Foster MJ, Mishra B. Compiling path expressions into VLSI circuits Distributed Computing. 1: 150-166. DOI: 10.1007/Bf01661169  0.537
1986 Clarke EM. Distributed computing issues in hardware design Distributed Computing. 1: 185-186. DOI: 10.1007/Bf01660030  0.364
1985 Sistla AP, Clarke EM. The Complexity of Propositional Linear Temporal Logics Journal of the Acm (Jacm). 32: 733-749. DOI: 10.1145/3828.3837  0.306
1985 Mishra B, Clarke E. Hierarchical verification of asynchronous circuits using temporal logic Theoretical Computer Science. 38: 269-291. DOI: 10.1016/0304-3975(85)90223-3  0.538
1984 Clarke EM. The characterization problem for Hoare logics Philosophical Transactions of the Royal Society A. 312: 423-440. DOI: 10.1098/Rsta.1984.0068  0.371
1984 Sistla AP, Clarke EM, Francez N, Meyer AR. Can message buffers be axiomatized in linear temporal logic? Information and Control. 63: 88-112. DOI: 10.1016/S0019-9958(84)80043-1  0.314
1982 Emerson EA, Clarke EM. Using branching time temporal logic to synthesize synchronization skeletons Science of Computer Programming. 2: 241-266. DOI: 10.1016/0167-6423(83)90017-5  0.555
1981 Roberts ES, Evans A, Morgan CR, Clarke EM. Task Management in Ada-A Critical Evaluation for Real-Time Multiprocessors Software - Practice and Experience. 11: 1019-1051. DOI: 10.1002/Spe.4380111004  0.392
1980 Clarke E. Synthesis of Resource Invariants for Concurrent Programs Acm Transactions On Programming Languages and Systems (Toplas). 2: 338-358. DOI: 10.1145/357103.357109  0.322
1980 Clarke EM. Proving correctness of coroutines without history variables Acta Informatica. 13: 169-188. DOI: 10.1007/Bf00263992  0.345
1979 Clarke EM. Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems Journal of the Acm. 26: 129-147. DOI: 10.1145/322108.322121  0.345
1979 Clarke EM. Program invariants as fixedpoints Computing. 21: 273-294. DOI: 10.1007/Bf02248730  0.322
Show low-probability matches.