Thesis

PDF format

Completeness and Incompleteness Theorems for Hoare-Like Axiom Systems (Sept 1976) [PDF]

Top

Papers Published in Refereed Journals

PDF format

Other formats

From non-preemptive to preemptive scheduling using synchronization synthesis.
Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach:
Formal Methods in System Design 50(2-3): 97-139 (2017)
PDF
Solving QBF with counterexample guided refinement.
Mikolás Janota, William Klieber, Joao Marques-Silva, Edmund M. Clarke:
Artif. Intell. 234: 1-25 (2016)
PDF
Pathway-gene identification for pancreatic cancer survival via doubly regularized Cox regression.
Haijun Gong, Tong Tong Wu, Edmund M. Clarke:
BMC Systems Biology 9(S-1): S3 (2014)
PDF
Bayesian statistical model checking with application to Stateflow/Simulink verification.
Paolo Zuliani, André Platzer, Edmund M. Clarke:
Formal Methods in System Design 43(2): 338-367 (2013)
PDF
Analysis and verification of the HMGB1 signaling pathway
Haijun Gong, Paolo Zuliani, Anvesh Komuravelli, James R. Faeder, Edmund M. Clarke:
BMC Bioinformatics 11(S-7): S10 (2010)
PDF
On simulation-based probabilistic model checking of mixed-analog circuits.
Edmund M. Clarke, Alexandre Donzé, Axel Legay:
Formal Methods in System Design 36(2): 97-113 (2010)
PDF
Model checking: algorithmic verification and debugging.
Edmund M. Clarke, E. Allen Emerson, Joseph Sifakis:
Commun. ACM 52(11): 74-84 (2009)
PDF
Functional Equivalence Verification Tools in High-Level Synthesis Flows.
Anmol Mathur, Masahiro Fujita, Edmund M. Clarke, Pascal Urard:
IEEE Design & Test of Computers 26(4): 88-95 (2009)
PDF
Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations.
Himanshu Jain, Edmund M. Clarke, Orna Grumberg:
Formal Methods in System Design 35(1): 6-39 (2009)
PDF
Computing differential invariants of hybrid systems as fixedpoints.
André Platzer, Edmund M. Clarke:
Formal Methods in System Design 35(1): 98-120 (2009)
PDF
Verification of evolving software via component substitutability analysis.
Sagar Chaki, Edmund M. Clarke, Natasha Sharygina, Nishant Sinha:
Formal Methods in System Design 32(3): 235-266 (2008)
PDF
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke:
IEEE Trans. on CAD of Integrated Circuits and Systems 27(2): 366-379 (2008)
PDF
Verification of SpecC using predicate abstraction.
Edmund M. Clarke, Himanshu Jain, Daniel Kroening:
Formal Methods in System Design 30(1): 5-28 (2007)
PDF
Model Checking: Software and Beyond.
Edmund M. Clarke, Flavio Lerda:
J. UCS 13(5): 639-649 (2007)
PDF
Concurrent software verification with states, events, and deadlocks.
Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha:
Formal Asp. Comput. 17(4): 461-483 (2005)

PDF
An Iterative Framework for Simulation Conformance.
Sagar Chaki, Edmund M. Clarke, Somesh Jha, Helmut Veith:
J. Log. Comput. 15(4): 465-488 (2005)
PDF
Computational challenges in bounded model checking.
Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman:
STTT 7(2): 174-183 (2005)
PDF
VeriAgent: an Approach to Integrating UML and Formal Verification Tools.
Edjard Mota, Edmund M. Clarke, Alex Groce, Waleska Oliveira, Marcia Falcăo, Jorge Kanda:
Electr. Notes Theor. Comput. Sci. 95: 111-129 (2004)
PDF
Predicate Abstraction of ANSI-C Programs Using SAT.
Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav:
Formal Methods in System Design 25(2-3): 105-127 (2004)
PDF
Efficient Verification of Sequential and Concurrent C Programs.
Sagar Chaki, Edmund M. Clarke, Alex Groce, Joël Ouaknine, Ofer Strichman, Karen Yorav:
Formal Methods in System Design 25(2-3): 129-166 (2004)
PDF
PS
SAT-based counterexample-guided abstraction refinement.
Edmund M. Clarke, Anubhav Gupta, Ofer Strichman:
IEEE Trans. on CAD of Integrated Circuits and Systems 23(7): 1113-1123 (2004)
PDF
Modular Verification of Software Components in C.
Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith:
IEEE Trans. Software Eng. 30(6): 388-402 (2004)
PDF
Bounded model checking.
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu:
Advances in Computers 58: 117-148 (2003)
PDF
Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach.
Sagar Chaki, Joël Ouaknine, Karen Yorav, Edmund M. Clarke:
Electr. Notes Theor. Comput. Sci. 89(3): 417-432 (2003)

[PDF]
Counterexample-guided abstraction refinement for symbolic model checking
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith:
JACM 50(5): 752-794 (2003)
[PDF]
Abstraction and counterexample-guided refinement in model checking of hybrid systems.
Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce Krogh, Joel Ouaknine, Olaf Stursberg, Michael Theobald:
International Journal of Foundations of Computer Science 14(4), 2003.
[PDF]
Efficient verification of sequential and concurrent C programs.
Sagar Chaki, Edmund M. Clarke, Alex Groce, Joel Ouaknine, Ofer Strichman, Karen Yorav:
Submitted to FMSD, 2003.
[PDF]
[PDF]
[PS]

Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function.
Sergey Berezin, Edmund M. Clarke, Armin Biere, Yunshan Zhu:
Formal Methods in System Design 20(2): 159-186 (2002)
[PDF]
Program slicing for VHDL
Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum:
STTT 4(1): 125-137 (2002)
[PS]
Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function
Clarke, E.M., Berezin, S., Biere, A., & Zhu, Y. with Sergey Berezin, Armin Biere, Yunshan Zhu.
Formal Methods In System Design, 2001.
[PDF]
Bounded Model Checking Using Satisfiability Solving
Edmund M. Clarke, Armin Biere, Richard Raimi, Yunshan Zhu:
Formal Methods in System Design 19(1): 7-34 (2001)
[PDF]
The Verus language: representing time efficiently with BDDs.
Sérgio Vale Aguiar Campos, Edmund M. Clarke:
Theor. Comput. Sci. 253(1): 95-118 (2001)
[PDF]
Formal Methods: State of the Art and Future Directions
Clarke, E.M. and Wing, Jeannette
[PDF]
[PS]
Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System
Clarke, E.M., Campos, S., & Grumberg, O.
Formal Methods In System Design, Vol. 17, No. 2, October 2000.
[PS]
NuSMV: A New Symbolic Model Checker
Clarke, E.M., Cimatti, A., Giumchiglia F., & Roveri, M.
Software Tools For Technology Transfer, Vol. 2 (4), p. 410, 2000.
[PDF]
[DOC]

[PS]
Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints
Hartonas-Garmhausen, V., Campos, S., Cimatti, A., Clarke, E., & Giunchiglia, F.
Science of Computer Programming, Vol. 36 (1), pp. 53-64, 2000.
[PDF]
Automatic verification of hardware and software systems.
Edmund M. Clarke:
ACM SIGSOFT Software Engineering Notes 25(1): 41-42 (2000)
[PDF]
Verifying security protocols with Brutus.
Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero:
ACM Trans. Softw. Eng. Methodol. 9(4): 443-487 (2000)
[PDF]
Verifying the SRT Division Algorithm Using Theorem Proving Techniques
(slightly skewed but very, very good scan, should be accepted)
Clarke, E.M., German, S., & Zhao, X.
Formal Methods In System Design, Vol. 14, No. 1, pp. 7-44, January 1999.
[PDF]
The Analysis and Verification of Real-Time Systems Using Quantitative Symbolic Algorithms
Clarke, E.M. and Campos, S.
International Journal of Software Tools for Technology Transfer, Vol. 2(3), p.260, 1999.
PDF
On the Semantic Foundations of Probabilistic Synchronous Reactive Programs.
Christel Baier, Edmund M. Clarke, Vasilili Hartonas-Garmhausen:
Electr. Notes Theor. Comput. Sci. 22: 3-28 (1999)
[PDF]
Combining Local and Global Model Checking.
Armin Biere, Edmund M. Clarke, Yunshan Zhu:
Electr. Notes Theor. Comput. Sci. 23(2): 34-45 (1999)
[PDF]
Model Checking Semi-Continuous Time Models Using BDDs.
Sérgio Vale Aguiar Campos, Marcio Teixeira, Marius Minea, Andreas Kuehlmann, Edmund M. Clarke:
Electr. Notes Theor. Comput. Sci. 23(2): 75-87 (1999)
[PDF]
State Space Reduction Using Partial Order Techniques
Clarke, E.M., Grumberg, O., Minea, M., Peled, D. 1998
[PDF]
Analytica: An Experiment in Combining Theorem Proving and Symbolic Computation
Clarke, E.M., Bauer, A., & Zhao, X.
Journal of Automated Reasoning, Vol. 21, p. 295, 1998.
[PDF]
Verifying Parameterized Networks
Clarke, E.M., Grumberg, O., & Jha, S.
ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 19, No. 5, pp.726-750, September 1997.
[PDF]
Symbolic Techniques for Formally Verifying Industrial Systems
Clarke, E.M., Campos, S., & Minea, M.
Science of Computer Programming, Vol. 29, No. 1-2, pp. 79-98, July 1997.
[PDF]
Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping
Clarke, E.M., Mcmillan, K., Zhao, X., Fujita M., & Yang, J.
Formal Methods In System Design, Vol. 10, No. 2/3, pp. 137-148, April/May 1997.
[PDF]
Another Look at LTL Model Checking
Clarke, E.M., Grumberg, O., & Hamaguchi, H.
Formal Methods In System Design, Vol. 10, No. 1, pp. 47-71, February 1997.
[PS]
An Improved Algorithm for Evaluation of Fixpoint Expressions
Clarke, E.M., Browne, A., Jha, S., Long, D., & Marrero, W.
Theoretical Computer Science, Vol. 178, pp. 237-255, 1997.
[PDF]
Editorial. Formal Methods in System Design
Edmund M. Clarke:
10(1): 5 (1997)
link
Symbolic Techniques for Formally Verifying Industrial Systems.
Sérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea:
Sci. Comput. Program. 29(1-2): 79-98 (1997)
[PDF]
Exploiting Symmetry in Temporal Logic Model Checking
Clarke, E.M., Enders, R., Filkorn T., & Jha, S.
Formal Methods In System Design, Vol. 9, No.1/2., pp. 77-104, August 1996.
[PDF]
Computer-Aided Verification
Clarke, E.M. & Kurshan, R.P.
IEEE Spectrum, Vol. 33 (6), pp. 61-67, June 1996.
[PDF]
[PS]
Tools and Partial Analysis.
Edmund M. Clarke, Jeannette M. Wing:
ACM Comput. Surv. 28(4es): 116 (1996)
link
Temporal Verification of Real-Time Systems
Campos, S., Clarke, E.M., Marrero, W., Minea, M., & Hiraishi, H.
IEICE Transactions on Information and Systems, Vol. E78-D, No. 7, pp. 796-802, July 1995.
[PDF]
Verification of the Futurebus+ Cache Coherence Protocol
Clarke, E.M., Grumberg, O., Hiraishi, H., Jha, S., Long, D., McMillan, K., & Ness, L.
Formal Methods In System Design, Vol. 6, No. 2, pp. 217-232, March 1995.
[PDF]
Model Checking and Abstraction
Clarke, E.M., Grumberg, O., & Long, D.E.
ACM TOPLAS, Vol. 16, No. 5, pp. 1512-1542, September 1994.
[PDF]
Symbolic Model Checking for Sequential Circuit Verification
(2nd paper is better but 1st has exact edition and date)
Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., & Dill, D.L.
IEEE Transactions On Computer-Aided Design of Intergrated Circuits and Systems, Vol. 13, No. 4, pp. 401-424, April 1994.
[PDF]

[PDF]
A Unified Approach for Showing Language Containment And Equivalence between Various Types of Omega-Automata
Clarke, E.M., Draghicescu, I.A., & Kurshan, R.P. Information Processing Letters, Vol. 46, pp. 301-308, 1993.
[PDF]
Application of BDDs to CAD for Digital Systems
Clarke, E.M. and Fujita, M. Journal of the Information Processing Society of Japan, Vol. 34, No. 5, pp. 609-616, May 1993.
Analytica: A Theorem Prover for Mathematica
Clarke, E.M., and Zhao, X.:
The Mathematica Journal, Vol. 3, No.1, pp.56-71, WInter 1993.
New and used temporal models: An issue of time.
Frank D. Anger, Edmund M. Clarke:
Appl. Intell. 3(1): 5-15 (1993)
[PDF]
A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems
Clarke, E.M., Grumberg, O., & Kurshan, R.P.
Journal of Logic and Computation, Vol. 2, No. 5, pp. 605-618, October 1992.
[PDF]
PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses
Bose, S., Clarke, E.M., Long, D.E., & Michaylov, S.
Journal of Automated Reasoning, Vol. 8, pp. 153-181, August 1992.
[PDF]
Symbolic Model Checking: 10^20 States and Beyond
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., & Hwang, J.
Information and Computation (Special issue for the best papers from LICS’90), Vol. 98, No. 2, pp. 142-170, June 1992.
[PDF]
Automatic Verification of Sequential Control Systems using Temporal Logic
(First paper is better than 2nd, but 2nd is the exact paper according to specs)
Clarke, E.M., Moon, I., Powers, G.J., & Burch, J.R.
American Institute of Chemical Engineers Journal, Vol. 38, No. 1, pp. 67-75, January 1992.
[PDF]
[PDF]
Reasoning about Procedures as Parameters in the Language L4
Clarke, E.M., German, S.M., & Halpern, J.Y.
Information and Computation, Vol. 83, No. 3, pp. 265-359, December 1989.
[PDF]
[PDF]
Reasoning about Networks with Many Identical Processes
Clarke, E.M., Browne, M., & Grumberg, O.
Information and Computation, Vol. 81, No. 1, pp. 13-31, April 1989.
[PDF]
Characterizing Finite Kripke Structures in Propositional Temporal Logic
Clarke, E.M., Browne, M.C., & Grumberg, O.
Theoretical Computer Science, Vol. 59, pp. 115-131, 1988.
[PDF]
Escher-A Geometrical Layout System for Recursively Defined Circuits
Clarke, E.M. and Feng, Y.
IEEE Transactions On Computer-Aided Design of Intergrated Circuits and Systems, Vol. 7, No. 8, pp. 908-919, August 1988.
[PDF]
Compiling Path Expressions into VLSI Circuits
Clarke, E.M., Anantharaman, T.S., Foster, M.J. & Mishra, B.
Distributed Computing, Vol. 1, No. 3, pp. 150-166, 1986.
[PDF]
Automatic Verification of Sequential Circuits Using Temporal Logic
Browne, M.C., Clarke, E.M., Dill, D.L., & Mishra, B.
IEEE Transactions On Computers, Vol. C-35, No. 12, pp. 1035-1044, December 1986.
[PDF]
Automatic Verification of Asynchronous Circuits Using Temporal Logic
Dill, D.L. and Clarke, E.M.
IEEE Procedings, Vol. 133, Pt. E, No. 5, pp. 276-282, September 1986.
[PDF]
Distributed Computing Issues in Hardware Design.
Edmund M. Clarke:
Distributed Computing 1(4): 185-186 (1986)
[PDF]
Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications
Clarke, E.M., Sistla, A.P., Francez, N., & Meyer, A.
ACM Transactions On Programming Languages and Systems, Vol. 8, No. 2, pp.244-263, 1986.
[PDF]
Hierarchical Verification of Asynchonous Circuits Using Temporal Logic
Clarke, E.M. and Mishra, B.
Theoretical Computer Science. Vol. 38, pp. 269-291, 1985.
[PDF]
The Complexity of Propositional Linear Temporal Logic
Clarke, E.M. and Sistla, A.P.
Journal of The Association for Computing Machinery. Vol. 32, No.3, pp.733-749, July 1985.
[PDF]
Can Message Buffers be Axiomatized in Linear Temporal Logic?
Clarke, E.M., Sistla, A.P., Francez, N., & Meyer, A.
Information and Control, Vol. 63, No. 1/2, pp. 88-112, October/November 1984.
[PDF]
On Effective Axiomatizations of Hoare Logics
Clarke, E.M., German, S.M., & Halpern, J.Y.
Journal of the Association for Computing Machinery, Vol. 30, No. 3, pp. 612-636, July 1983.
[PDF]
[PDF]
Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons
Clarke, E.M. and Emerson, E.A.
Science of Computing 2, pp. 241-266, 1982.
[PDF]
Distributed Reconfiguration Strategies for Fault Tolerant Multiprocessor Systems
Clarke, E.M. and Nikolaou, C.N.
IEEE Transactions On Computers (Special Issue on Fault Tolerant Computing), Vol. C-31, No. 8, August 1982.
[PDF]
Task Management in Ada-A Critical Evaluation for Real-Time Multiprocessors
Clarke, E.M., Evans, A., Morgan, R., & Roberts. E.
Software: Practice and Experience, Vol. 11, pp. 1019-1051, 1981.
[PDF]
Proving the Correctness of Coroutines Without History Variables
Clarke, E.M.
Acta Informatica, Vol.13, pp. 169-188, 1980.
[PDF]
Synthesis of Resource Invariants for Concurrent Programs
Clarke, E.M.
ACM TOPLAS, Vol. 2, No. 3, pp. 338-358, July 1980.
[PDF]

[PDF]
Program Invariants as Fixed Points
Clarke, E.M.
Computing, Vol. 21, No.4, pp. 273-294, 1979.
[PDF]
Programming Language Constructs for Which it is Impossible to Obtain Good Hoare-like Axiom Systems
Clarke, E.M.
Journal of the Association for Computing Machinery, Vol. 26, No. l, pp. 129-147, January 1979.
[PDF]

Top

Papers Presented at Refereed Conferences and Workshops

PDF format

Other formats

CyberCardia project: Modeling, verification and validation of implantable cardiac devices.
Md. Ariful Islam, Hyun-Kyung Lim, Nicola Paoletti, Houssam Abbas, Zhihao Jiang, Jacek Cyranka, Rance Cleaveland, Sicun Gao, Edmund M. Clarke, Radu Grosu, Rahul Mangharam, Elizabeth Cherry, Flavio H. Fenton, Richard A. Gray, James Glimm, Shan Lin, Qinsi Wang, Scott A. Smolka:
CMSB 2016: 132-146
[PDF]
Bifurcation Analysis of Cardiac Alternans Using delta-Decidability.
Md. Ariful Islam, Greg Byrne, Soonho Kong, Edmund M. Clarke, Rance Cleaveland, Flavio H. Fenton, Radu Grosu, Paul L. Jones, Scott A. Smolka:
BIBM 2016: 1445-1452
[PDF]
Formal Modeling and Analysis of Pancreatic Cancer Microenvironment.
Qinsi Wang, Natasa Miskov-Zivanov, Bing Liu, James R. Faeder, Michael Lotze, Edmund M. Clarke:
CMSB 2016: 289-305
[PDF]
High-level modeling and verification of cellular signaling.
Natasa Miskov-Zivanov, Paolo Zuliani, Qinsi Wang, Edmund M. Clarke, James R. Faeder:
HLDVT 2016: 162-169
[PDF]
Probabilistic reachability analysis of the tap withdrawal circuit in caenorhabditis elegans.
Md. Ariful Islam, Qinsi Wang, Ramin M. Hasani, Ondrej Balun, Edmund M. Clarke, Radu Grosu, Scott A. Smolka:
HLDVT 2016: 170-177
[PDF]
Formal modeling of biological systems.
Qinsi Wang, Edmund M. Clarke:
HLDVT 2016: 178-184
[PDF]
SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems.
Kyungmin Bae, Peter Csaba Ölveczky, Soonho Kong, Sicun Gao, Edmund M. Clarke:
HSCC 2016: 145-154
[PDF]
From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis.
Pavol Cerný, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach:
CAV (2) 2015: 180-197
[PDF]
SReach: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems.
Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao, Edmund M. Clarke:
CMSB 2015: 15-27
[PDF]
Formal Analysis Provides Parameters for Guiding Hyperoxidation in Bacteria using Phototoxic Proteins.
Qinsi Wang, Natasa Miskov-Zivanov, Cheryl Telmer, Edmund M. Clarke:
ACM Great Lakes Symposium on VLSI 2015: 315-320
[PDF]
Towards personalized prostate cancer therapy using delta-reachability analysis.
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke:
HSCC 2015: 227-232
[PDF]
dReach: Delta-Reachability Analysis for Hybrid Systems
Soonho Kong, Sicun Gao, Wei Chen, and Edmund Clarke:
TACAS 2015
[PDF]
Towards Personalized Prostate Cancer Therapy Using Delta-Reachability Analysis
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke:
HSCC 2015
[PDF]
Model checking for studying temporal behavior in cell differentiation
Natasa Miskov-Zivanov, Paolo Zuliani, Penelope Morel, Edmund M. Clarke, James R. Faeder:
q-bio Conference on Cellular Information Processing, August 2012
[PDF]
Studies of biological networks with statistical model checking: application to immune system cells.
Natasa Miskov-Zivanov, Paolo Zuliani, Edmund M. Clarke, James R. Faeder:
BCB 2013: 728
[PDF]
dReal: An SMT Solver for Nonlinear Theories over the Reals.
Sicun Gao, Soonho Kong, Edmund M. Clarke:
CADE 2013: 208-214
[PDF]
Automatic Abstraction in SMT-Based Unbounded Software Model Checking.
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke:
CAV 2013: 846-862
[PDF]
Solving QBF with Free Variables.
William Klieber, Mikolás Janota, Joao Marques-Silva, Edmund M. Clarke:
CP 2013: 415-431
[PDF]
Satisfiability modulo ODEs.
Sicun Gao, Soonho Kong, Edmund M. Clarke:
FMCAD 2013: 105-112
[PDF]
Finding Errors in Python Programs Using Dynamic Symbolic Execution.
Samir Sapra, Marius Minea, Sagar Chaki, Arie Gurfinkel, Edmund M. Clarke:
ICTSS 2013: 283-289
[PDF]
Turing's Computable Real Numbers and Why They Are Still Important Today.
Clarke, E.M.
SAT 2013: 18
VIDEO
Delta-Complete Decision Procedures for Satisfiability over the Reals.
Sicun Gao, Jeremy Avigad, Edmund M. Clarke:
IJCAR 2012: 286-300
[PDF]
Assume-Guarantee Abstraction Refinement for Probabilistic Systems.
Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke:
CAV 2012: 310-326
[PDF]
Assumption Generation for Asynchronous Systems by Abstraction Refinement.
Qiusong Yang, Edmund M. Clarke, Anvesh Komuravelli, Mingshu Li:
FACS 2012: 260-276
[PDF]
Rare-event verification for stochastic hybrid systems.
Paolo Zuliani, Christel Baier, Edmund M. Clarke:
HSCC 2012: 217-226
[PDF]
Delta-Decidability over the Reals.
Sicun Gao, Jeremy Avigad, Edmund M. Clarke:
LICS 2012: 305-314
[PDF]
Learning Probabilistic Systems from Tree Samples.
Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke:
LICS 2012: 441-450
[PDF]
Statistical Model Checking for Markov Decision Processes.
David Henriques, Joăo Martins, Paolo Zuliani, André Platzer, Edmund M. Clarke:
QEST 2012: 84-93
[PDF]
Solving QBF with Counterexample Guided Refinement.
Mikolás Janota, William Klieber, Joăo Marques-Silva, Edmund M. Clarke:
SAT 2012: 114-128
[PDF]
Analog circuit verification by statistical model checking.
Ying-Chih Wang, Anvesh Komuravelli, Paolo Zuliani, Edmund M. Clarke:
ASP-DAC 2011: 1-6
[PDF]
Statistical Model Checking for Cyber-Physical Systems.
Edmund M. Clarke, Paolo Zuliani:
ATVA 2011: 1-12
[PDF]
Quantifier Elimination over Finite Fields Using Gröbner Bases.
Sicun Gao, André Platzer, Edmund M. Clarke:
CAI 2011: 140-157
[PDF]
Formal analysis for logical models of pancreatic cancer.
Haijun Gong, Paolo Zuliani, Qinsi Wang, Edmund M. Clarke:
CDC-ECE 2011: 4855-4860
[PDF]
Model Checking and the State Explosion Problem.
Edmund M. Clarke, William Klieber, Milos Novácek, Paolo Zuliani:
LASER Summer School 2011: 1-30
[PDF]
Computational Modeling and Verification of Signaling Pathways in Cancer.
Haijun Gong, Paolo Zuliani, Anvesh Komuravelli, James R. Faeder, Edmund M. Clarke:
ANB 2010: 117-135
[PDF]
The Localization Reduction and Counterexample-Guided Abstraction Refinement.
Edmund M. Clarke, Robert P. Kurshan, Helmut Veith:
Essays in Memory of Amir Pnueli 2010: 61-71
[PDF]
Automated Assume-Guarantee Reasoning through Implicit Learning.
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang:
CAV 2010: 511-526
[PDF]
Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems.
Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke:
FMCAD 2010: 81-89
[PDF]
Bayesian statistical model checking with application to Simulink/Stateflow verification.
Paolo Zuliani, André Platzer, Edmund M. Clarke:
HSCC 2010: 243-252
[PDF]
Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning.
Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, Lei Zhu:
ISoLA (1) 2010: 643-657
[PDF]
A Non-prenex, Non-clausal QBF Solver with Game-State Learning.
William Klieber, Samir Sapra, Sicun Gao, Edmund M. Clarke:
SAT 2010: 128-142
[PDF]
Statistical Verification of Probabilistic Properties with Unbounded Until.
Hĺkan L. S. Younes, Edmund M. Clarke, Paolo Zuliani:
SBMF 2010: 144-160
[PDF]
A Bayesian Approach to Model Checking Biological Systems.
Sumit Kumar Jha, Edmund M. Clarke, Christopher James Langmead, Axel Legay, André Platzer, Paolo Zuliani:
CMSB 2009: 218-234
[PDF]
Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts.
Himanshu Jain, Edmund M. Clarke:
DAC 2009: 563-568
[PDF]
Formal Verification of Curved Flight Collision Avoidance Maneuvers
André Platzer, Edmund M. Clarke:
A Case Study. FM 2009: 547-562
[PDF]
My 27-year Quest to Overcome the State Explosion Problem.
Edmund M. Clarke:
LICS 2009: 3
[PPT]
Model Checking - My 27-year Quest to Overcome the State Explosion Problem.
Edmund M. Clarke:
NASA Formal Methods 2009: 1
Learning Minimal Separating DFA's for Compositional Verification.
Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang:
TACAS 2009: 31-45
[PDF]
Computing Differential Invariants of Hybrid Systems as Fixedpoints.
André Platzer, Edmund M. Clarke:
CAV 2008: 176-189
[PDF]
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations.
Himanshu Jain, Edmund M. Clarke, Orna Grumberg:
CAV 2008: 254-267
[PDF]
Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway.
Edmund M. Clarke, James R. Faeder, Christopher James Langmead, Leonard A. Harris, Sumit Kumar Jha, Axel Legay:
CMSB 2008: 231-250
[PDF]
Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator.
Edmund M. Clarke, Alexandre Donzé, Axel Legay:
Haifa Verification Conference 2008: 149-163
[PDF]
Verification of Supervisory Control Software Using State Proximity and Merging.
Flavio Lerda, James Kapinski, Edmund M. Clarke, Bruce H. Krogh:
HSCC 2008: 344-357
[PDF]
Model Checking - My 27-Year Quest to Overcome the State Explosion Problem.
Edmund M. Clarke:
LPAR 2008: 182
VIDEO
The Birth of Model Checking.
Edmund M. Clarke:
25 Years of Model Checking 2008: 1-26
[PDF]
Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic.
Edmund M. Clarke, E. Allen Emerson:
25 Years of Model Checking 2008: 196-215
[PDF]
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages.
Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang:
TACAS 2008: 2-17
[PDF]
Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems.
Edmund M. Clarke, Muralidhar Talupur, Helmut Veith:
TACAS 2008: 33-47
[PDF]
SAT-Based Compositional Verification Using Lazy Learning.
Nishant Sinha, Edmund M. Clarke:
CAV 2007: 39-54
[PDF]
Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction.
Sumit Kumar Jha, Bruce H. Krogh, James E. Weimer, Edmund M. Clarke:
HSCC 2007: 287-300
[PDF]
The Image Computation Problem in Hybrid Systems Model Checking.
André Platzer, Edmund M. Clarke:
HSCC 2007: 473-486
[PDF]
Arithmetic Strengthening for Shape Analysis.
Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook:
SAS 2007: 419-436
[PDF]
Satisfiability Checking of Non-clausal Formulas Using General Matings.
Himanshu Jain, Constantinos Bartzis, Edmund M. Clarke:
SAT 2006: 75-89
[PDF]
Ranking Attack Graphs.
Vaibhav Mehta, Constantinos Bartzis, Haifeng Zhu, Edmund M. Clarke, Jeannette M. Wing:
RAID 2006: 127-144
[PDF]
Verifying Concurrent Message-Passing C Programs with Recursive Calls.
Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili:
TACAS 2006: 334-349
[PDF]
Environment Abstraction for Parameterized Verification.
Edmund M. Clarke, Muralidhar Talupur, Helmut Veith:
VMCAI 2006: 126-141
[PDF]
Automated Assume-Guarantee Reasoning for Simulation Conformance.
Sagar Chaki, Edmund M. Clarke, Nishant Sinha, Prasanna Thati:
CAV 2005: 534-547
[PDF]
Word level predicate abstraction and refinement for verifying RTL verilog.
Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke:
DAC 2005: 445-450
[PDF]
Dynamic Component Substitutability Analysis.
Natasha Sharygina, Sagar Chaki, Edmund M. Clarke, Nishant Sinha:
FM 2005: 512-528
[PDF]
Program Compatibility Approaches.
Edmund M. Clarke, Natasha Sharygina, Nishant Sinha:
FMCO 2005: 243-258
[PDF]
Refining Abstractions of Hybrid Systems Using Counterexample Fragments.
Ansgar Fehnker, Edmund M. Clarke, Sumit Kumar Jha, Bruce H. Krogh:
HSCC 2005: 242-257
[PDF]
Reconsidering CEGAR: Learning Good Abstractions without Refinement.
Anubhav Gupta, Edmund M. Clarke:
ICCD 2005: 591-598
[PDF]
State/Event Software Verification for Branching-Time Specifications.
Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith:
IFM 2005: 53-69
[PDF]
SATABS: SAT-Based Predicate Abstraction for ANSI-C.
Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav:
TACAS 2005: 570-574
[PDF]
Grand Challenge: Model Check Software.
Edmund M. Clarke, Himanshu Jain, Nishant Sinha:
VISSAS 2005: 55-68
[PDF]
Model Checking: Back and Forth between Hardware and Software.
Edmund M. Clarke, Anubhav Gupta, Himanshu Jain, Helmut Veith:
VSTTE 2005: 251-255
[PDF]
Verification by Network Decomposition.
Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, Helmut Veith:
CONCUR 2004: 276-291
[PDF]
A SAT-based algorithm for reparameterization in symbolic simulation.
Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening:
DAC 2004: 524-529
[PDF]
Checking consistency of C and Verilog using predicate abstraction and induction.
Daniel Kroening, Edmund M. Clarke:
ICCAD 2004: 66-72
[PDF]
Tutorial: Software Model Checking.
Edmund M. Clarke, Daniel Kroening:
ICFEM 2004: 9-10
[PDF]
Counterexample Guided Abstraction Refinement Via Program Execution.
Daniel Kroening, Alex Groce, Edmund M. Clarke:
ICFEM 2004: 224-238
[PDF]
State/Event-Based Software Model Checking.
Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha:
IFM 2004: 128-147
[PDF]
[PS]
Verification of SpecC using predicate abstraction.
Himanshu Jain, Daniel Kroening, Edmund M. Clarke:
MEMOCODE 2004: 7-16
[PDF]
Automated, compositional and iterative deadlock detection.
Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina:
MEMOCODE 2004: 201-210
[PDF]
A Tool for Checking ANSI-C Programs.
Edmund M. Clarke, Daniel Kroening, Flavio Lerda:
TACAS 2004: 168-176
[PDF]
Completeness and complexity of bounded model checking.
Edmund M. Clarke, Daniel Kroening, Joel Ouaknine, Ofer Strichman:
VMCAI 2004, LNCS (to appear).
[PDF]
[PS]
Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates
Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang
CAV 2003: 126-140
[PDF]
Behavioral consistency of C and verilog programs using bounded model checking
Edmund M. Clarke, Daniel Kroening, Karen Yorav:
DAC 2003: 368-371
[PDF]
[PDF]
Modular Verification of Software Components in C.
Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith:
ICSE 2003: 385-395
[PDF]
[PS]
Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement.
Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Olaf Stursberg, Michael Theobald:
TACAS 2003: 192-207
[PDF]
State/event-based software model checking
Edmund M. Clarke, Joel Ouaknine, Natasha Sharygina, Nishant Sinha:
Submitted to IFM 2003.
[PDF]
[PS]
Automated compositional abstraction refinement for concurrent C programs: A two-level approach.
Sagar Chaki, Edmund M. Clarke, Joel Ouaknine, Karen Yorav:
Proceedings of SoftMC 2003, ENTCS 89(3).
[PDF]
[PS]
System description: Analytica 2.
Edmund M. Clarke, Michael Kohlhase, Joel Ouaknine, Klaus Sutner:
CALCULEMUS 2003.
[PDF]
[PS]
Specifying and Verifying Systems with Multiple Clocks
Edmund M. Clarke, Daniel Kroening, Karen Yorav:
ICCD 2003 (to appear).
[PDF]
Predicate Abstraction of ANSI-C Programs using SAT.
Edmund M. Clarke, Daniel Kroening, Natalia Sharygina, Karen Yorav:
Proceedings of the Model Checking for Dependable Software-Intensive Systems Workshop, San-Francisco, USA, 2003.
[PDF]
Hardware Verification using ANSI-C Programs as a Reference
Edmund M. Clarke, Daniel Kroening:
ASP-DAC 2003: 308-311.
[PDF]
VeriAgent: an Approach to Integrating UML and Formal Verification Tools.
Edjard Mota, Edmund M. Clarke, W. Oliveira, Alex Groce, J. Kanda, and M. Falcao.
VMF 2003 (to appear).
[PS]
Predicate Abstraction with Minimum Predicates.
Sagar Chaki, Edmund M. Clarke, Alex Groce, Ofer Strichman:
CHARME 2003, LNCS (to appear).
[PDF]

[PDF]
[PS]
Counterexamples Revisited: Principles, Algorithms, Applications.
Edmund M. Clarke, Helmut Veith:
Verification: Theory and Practice 2003: 208-224
[PDF]
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking.
Edmund M. Clarke:
CADE 2003: 1
[PDF]
Predicate Abstraction with Minimum Predicates.
Sagar Chaki, Edmund M. Clarke, Alex Groce, Ofer Strichman:
CHARME 2003: 19-34
[PDF]
[PS]
Model Checking for Dependable Software-Intensive Systems.
Edmund M. Clarke, Masahiro Fujita, David P. Gluch:
DSN 2003: 764
SAT-Based Algorithms for Logic Minimization.
Samir Sapra, Michael Theobald, Edmund M. Clarke:
ICCD 2003: 510-
[PDF]
High Level Verification of Control Intensive Systems Using Predicate Abstraction.
Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang:
MEMOCODE 2003: 55-64
[PDF]
SAT Based Predicate Abstraction for Hardware Verification.
Edmund M. Clarke, Muralidhar Talupur, Helmut Veith, Dong Wang:
SAT 2003: 78-92
[PDF]
Counterexample-Guided Abstraction Refinement.
Edmund M. Clarke:
TIME 2003: 7
[PDF]
[PS]
SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques
Edmund M. Clarke, Anubhav Gupta, James H. Kukula, Ofer Shrichman:
CAV 2002: 265-279
[PDF]
NuSMV 2: An OpenSource Tool for Symbolic Model Checking.
Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella:
CAV 2002: 359-364
[PDF]
[PS]
SAT-Based Counterexample Guided Abstraction Refinement
Edmund M. Clarke:
SPIN 2002: 1
[PDF]
Automated Abstraction Refinement for Model Checking Large Spaces using SAT based Conflict Analysis
Clarke, E.M., Chauhan, P., Sapra, S., Kakula, J., Veith, H., & Wang, D. To appear in Proceedings:
Fourth International Conference on Formal Methods in Computer-Aided Design 2002 (FMCAD2002), 2002.
[PDF]
TOOL Paper NuSMV2: an Open Source Tool for Symbolic Model Checking
Clarke, E.M., Cimatti, A., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., & Tacchella, A.
To appear in Proceedings: Conference on Computer-Aided Verification 2002 (CAV 2002), Copenhagen Denmark, July 27-21 2002.
[PDF]
[PS]
Tree-like Counterexamples in Model Checking
Clarke, E.M., Jha, S., Lu, Y., & Veith H.
Proceedings: IEEE Symposium on Logic in Computer Science 2002 (LICS '02), 2002.
[PS]
Failed Attempt to Optimize Variable Ordering with Tools for Constraints Solving
Edmund M. Clarke and Ofer Strichman:
CFV 2002.
[PS]
Using Combinatorial Optimization Methods for Quantification Scheduling
Pankay Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Helmut Veith, Dong Wang:
Conference Proceedings: Conference on Correct Hardware Design and Verification Methods (CHARME '01), Livingston Scotland, September 4-7, 2001. pp 293-309
[PDF]

[PDF]
Using Cutwidth to Improve Symbolic Simulation and Boolean Satisfiability
Wang, D., Clarke, E, Zhu, Y., & Kukula, J.
Proceedings: IEEE International High Level Design Validation and Test Workshop (HLDVT'01), 2001.
[PS]

Non-linear Quantification Scheduling in Image Computation
Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Thomas R. Shiple, Helmut Veith, Dong Wang:
International Conference on Computer Aided Design 2001 (ICAAD ’01), pp. 293 -298, 2001.
[PDF]
[PDF]
Efficient Filtering in Publish Subscribe Systems using Binary Decision Diagrams
Campailla, A., Chaki, S., Clarke, E., Jha, S., & Veith, H. Proceedings:
International Conference on Software Engineering (ICSE01), 2001.
[PDF]
[PS]
Progress on the State Explosion Problem in Model Checking.
Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith:
Informatics 2001: 176-194
[PDF]
Executable Protocol Specification in ESL
Clarke, E.M., German, S.M., Lu, Y., Veith, H., & Wang, D.
FMCAD 2000: 197-216, Austin, Texas, November 1-3 2000.
[PDF]
A Theory of Consistency for Modular Synchronous Systems
Clarke, E.M., Bryant, R.E., Chauhan, P., & Goel, A.
FMCAD 2000: 486-504, Austin, Texas, November 1-3 2000.
[PDF]
[PS]
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking
Clarke, E.M., Williams, P.F., Biere, A., & Gupta, A.
Carnegie Mellon University, Computer Science Department, Technical Report, CMU-CS-00-110, February 2000. Conference Proceedings: Computer Aided Verification (CAV ‘00), Chicago, IL, 2000.
[PDF]
[PS]
Efficient Variable Ordering Using a BDD Based Sampling Scheme
Lu. Y,. Jain, J., Clarke, E. & Fujita, M.
Proceedings: Design Automation Conference (DAC ’00), 2000.
[PDF]
Counterexample-guided Abstraction Refinement
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., & Veith, H.
Lecture Notes in Computer Science (2000). Proceedings: Computer Aided Verification (CAV ’00), Chicago, IL, 2000.

PDF]
[PS]
[PS]
Partial Order Reductions for Security Protocol Verification
Clarke, E.M., Jha, S., & Marrero, W.
Conference Proceedings: Tools and Algorithms for Construction and Analysis of Systems (TACAS'00), pp. 503-518, 2000.
[PDF]
 
Model Checking Algorithms for the u-Calculus
Clarke, E.M, Berezin, S., Marrero, W., Somesh, J.
Proof, Language, and Interaction, Edited by G. Plotkin, MIT Press, 2000.
[PDF]
Improving BDD Variable Ordering Using Abstract BDDs and Sampling
Clarke, E.M., Lu, Y., Jain, J., & Fujita, M.
Proceedings of International Workshop of High Level Design, Verification and Testing, (HLDVT), San Diego, California November 4-6 1999.
[PDF]
Verifying Safety Properties of a Power PC™ Microprocessor Using Symbolic Model Checking Without BDDs
Biere, A., Clarke, E.M., Raimi. R., & Zhu, Y.
Computer Aided Verificatioin (CAV 99), Trento, Italy, No. 1633, p. 60, July 7-10 1999.
[PDF]
Combining Local and Global Model Checking
Clarke, E.M., Biere, A., & Zhu, Y.
International Workshop on Symbolic Model Checking (SMC’99), pp. 75-87 Trento, Italy, July 1999.
[PDF]
[PS]
Model Checking Semi-Continuous Time Models Using BDDs
Clarke, E.M., Campos, S., Teixeira, M., Minea, M., & Kuehlman, A.
First International Workshop on Symbolic Model Checking (SMC '99), pp. 75-87, Trento, Italy, July 1999.
[PS]
NuSMV: A New Symbolic Model Verifier
Clarke, E.M., Cimatti, A., Giunchiglia, F., & Roveri, M.
Lecture Notes in Computer Science, Proceedings: Eleventh Conference on Computer-Aided Verification (CAV 99), Trento, Italy, July, No. 1633, pp. 495-499, 1999.
[PS]
[PS]
ProbVerus: Probabilistic Symbolic Model Checking
Clarke, E.M., Hartonas-Garmhausen, V., & Campos, S.
Lecture Notes in Computer Science, no. 1601 (1999). 5th International AMAST Workshop on Real-Time and Probabilistic Systems, Bamberg, Germany, May 1999. Also in Proceedings(ARTS '99), 1999.
[PDF]
Verifying IP-Core Based System-On-Chip Design
Chauhan, P., Clarke, E.M., Lu, Y., & Wang, D. Proceedings:
12th Annual IEEE International ASIC/SOC Conference, pp. 27-31, 1999.
[PDF]
[PS]
Program Slicing of Hardware Description Languages
Clarke, E.M., Fujita, M., Rajan, S.P., Reps, T., Shankar, S., &Teitelbaum, T.
Conference on Correct Hardware Design and Verification Methods (CHARME 99), pp. 298-312, 1999.
[PDF]
A Technique for Using Abstraction in Model Checking
Clarke, E.M., Jha, S., Lu, Y., & Wang, D.
Conference on Correct Hardware Design and Verification Methods (CHARME 99), Vol. 1703, pp.172-186, 1999.
[PDF]
Symbolic Model Checking Using SAT Procedures Instead of BDDs
Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., & Zhu, Y.
Proceedings: Design Automation Conference (DAC '99), pp. 317-320, 1999.
[PDF]
Symbolic Model Checking Without BDDs
Clarke, E.M., Biere, A., Cimatti, A., and Zhu, Y.
Lecture Notes in Computer Science, Proceedings: Tools and Algorithms for Construction and Analysis of Systems (TACAS ’99), No. 1579, pp. 193-207, 1999.
[PDF]
[PS]
Multiple State and Single State Tableaux for Combining Local and Global Model Checking.
Armin Biere, Edmund M. Clarke, Yunshan Zhu:
Correct System Design 1999: 163-179
[PDF]
Analysis and Verification of Real-Time Systems Using Quantitative Symbolic Algorithms
Clarke, E.M., & Campos, S.
Software Tools for Technology Transfer (STTT ’98) pp. 25-32, Aalborg, Denmark, July 12-13, 1998.
[PDF]
Symmetry Reductions in Model Checking
Clarke, E.M., Emerson, E.A., Jha, S., & Sistla, A.P.
10th Internatioal Conference on Computer Aided Verifitcation (CAV '98), Vancouver, British Columbia, June/July 1998.
[PDF]
A Machine Checkable Logic of Knowledge for Specifying Security Properties of Electronic Commerce Protocols
Clarke, E., Jha, S., & Marrero, W.
13th IEEE Annual Symposium on Logic in Computer Science (LICS ‘98) Workshop on Formal Methods and Security Protocols, Indianapolis, Indiana, June 21-24 1998.
[slides]
[PDF]
Model-Checking VHDL with CV
Clarke, E.M., Deharbe, D. & Shankar, S.
Formal Methods In Computer-Aided Design. Also appears in Lecture Notes in Computer Science, no. 1522, pp. 508-514, 1998.
[PDF]
The Algebraic Mu-Calculus and MTBDDs
Clarke, E.M.& Christel Baier.
Proceedings 5th Workshop on Logic, Language, Information and Computation (WoLLIC '98), Sao Paulo, Brazil, pp. 27-38, 1998.
[PDF]
NuSMV: A reimplementation of SMV
Clarke, E.M., Cimatti, A., Giunchiglia, F., & Roveri, M.
Proceedings: 1st Feature Integration in Requirements Engeering (FIREworks '98), 1998.
[PDF]
Using Formal methods for Analyzing Security
Clarke, E.M., & Marrero, W.
Information Survivability Workshop, sponsored by IEEE Computer Society. pp. 37-41, 1998.
Formal Verification of VHDL - The Model Checker CV
Deharbe, D., Shankar, S., & Clarke, E.M.
Proceedings: XI Brazilian Symposium on Integrated Circuit Design (SBCCI ‘98), pp. 95-98, 1998.
[PDF]
Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols
Clarke, E.M., Jha, S. & Marrero, W.
Proceedings of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET),Shelter Island, New York, pp. 96-106, 1998
[PDF]
On the Semantic Foundations of Probabilistic VERUS
Clarke, E.M., Baier, C., & Hartonas-Garmhausen, V.
Electronic Notes in Computer Science,vol. 22, (1998). Proceedings: Workshop on Probabilistic Methods in Verification (PROBMIV ’98) Indianapolis, Indiana. Appears in Technical Report CSR-98-4, University of Birmingham, pp. 7-32, 1998.
[PS]
Symbolic Model Checking
Clarke, E.M., McMillan, K., & Campos, S. XXV Seminario Integrado de Software and Hardware, Sociedade Brasileira do Computacao, vol. 1, pp. 14-18, 1998.
[PDF]
Verification of a Safety-Critical Railway Interlocking System, with Real-time Constraints
Hartonas-Garmhausen, V., Campos, S., Cimatti, A., Clarke, E., & Giunchiglia, F.
Proceedings: 28th International Symposium on Fault-Tolerant Computing (FTCS-28), 1998.
[PS]
Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification
Clarke, E.M., Bezerin, S., Biere, A., & Zhu, Y.
Lecture Notes in Computer Science, No. 1522, pp. 369-38, Springer-Verlag (1998). Conference Proceedings Published of Collection: International Conference on Formal Methods in COmputer-Aided Design (FMCAD '98), Palo Alto CA, 1998.
[PDF]
Equivalence Checking Using Abstract BDDs
Jha, S., Lu, Y., Minea, M., & Clarke, E.M.
International Conference on Computer Design (ICCD 97), Austin, Texas, October, 1997, pp. 332-337.
[PDF]
A Model Checker for Authentication Protocols
Clarke, E.M., Marrero, W. & Jha, S.
Proceedings: (DIMACS) Workshop on Design and Formal Verification of Security Protocols, DIMACS Center, CoRE Building, Rutgers University, Piscataway, NJ, September 3-5, 1997.
[PDF]
[PS]
The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems
Clarke, E.M., S. Campos, M. Minea
Computer Aided Verification 9th International conference (CAV ’97). Haifa, Israel, Vol. 1254, June, 1997.
[PS]
Model Checking for Security Protocols
Marrero, W., Clarke, E.M., Jha,S.
DIMACS Workshop on Design and Formal Verication of Security Protocols, 1997. Preliminary version appears as Technical Report TR-CMU-CS-97-139, Carnegie Mellon University, May 1997.
[PDF]
[PS]
Hybrid Spectral Transform Diagrams
Clarke, E.M., Fujita, M., & Heinle, W.
Proceedings: First International Conference on Information, Communications and Signal Processing (ICICS ’97), Vol.1, pp. 251 -255, 1997.
[PDF]
Symbolic Model Checking for Probabilistic Processes
Clarke, E.M., Baier, C., Hartonas-Garmhausen, V., Kwiatkowska, M., & Ryan, M.
(ICALP '97): Automata, Languages and Programming (LNCS 1256), pages 430-437, 1997.
[PDF]
The Verus language: representing time efficiently with BDDs
Clarke, E.M., & Campos, S.
Fourth AMAST Workshop on Real-Time Systems, Concurrent, and Distributed Software, 1997. Submitted to Theoretical Computer Science.
[PS]
[PS]
Compositional Reasoning in Model Checking.
Sergey Berezin, Sérgio Vale Aguiar Campos, Edmund M. Clarke:
COMPOS 1997: 81-102
[PDF]
Model Checking.
Edmund M. Clarke:
FSTTCS 1997: 54-56
[PDF]
Equivalence Checking Using Abstract BDDs.
Somesh Jha, Yuan Lu, Marius Minea, Edmund M. Clarke:
ICCD 1997: 332-337
[PDF]
Temporal Logic Model Checking (Abstract)
Edmund M. Clarke:
ILPS 1997: 3
Symbolic Model Checking.
Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vassili Hartonas-Garmhausen:
CAV 1996: 419-427
[PDF]
Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking.
Yirng-An Chen, Edmund M. Clarke, Pei-Hsin Ho, Yatin Vasant Hoskote, Timothy Kam, Manpreet Khaira, John W. O'Leary, Xudong Zhao:
FMCAD 1996: 19-33
[PDF]
[PS]
Verification of All Circuits in a Floating-point Unit Using Word-level Model Checking
Clarke, E.M., Chen, Y., Ho, P., Hoskote, Y., Kam, T., Khaira, M., O'Leary, J., & and Zhao, X.
Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), Palo Alto, CA, November 1996.
[PDF]
[PS]
[PS]
Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation
Clarke, E.M., Bauer, A., & Zhao, X.
International Conference on Artificial Intelligence and Symbolic Mathematical Computation, AISMC-3, Steyr, pp.21-37, Austria, September 1996.
[PS]
[PS]
Verifying the SRT Division Algorithm using Theorem Proving Techniques
Clarke, E.M., German, S., and Zhao, X.
8th International Conference on Computer Aided Verification, CAV '96, New Brunswick, NJ, pp. 111-122, July/August, 1996.
[PDF]
Word-Level Symbolic Model Checking--A New Approach for Verifying Arithmetic Circuits
Clarke, E.M., Khaira M., & Zhao, X.
Proceedings: 33rd (ACM/IEEE) Design Automation Conference, 1996.
[PDF]
Deadlock Prevention in Flexible Manufacturing Systems Using Symbolic Model Checking
Hartonas-Garmhausen, V., Clarke, E.M., & Campos, S.
Proceedings: 1996 IEEE International Conference of Robotics and Automation, Vol. 1, pp. 527 -532, 1996.
[PDF]
Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols
Clarke, E. M., Jha, S. and Marrero, W.
IFIP 1996.
[PDF]
Formally Verifying Arithmetic Circuits - Avoiding the Pentium FDIV Bug
Campos, S., Khaira, M., Zhao, X., and Clarke, E.M.
Intel Design and Test Technology Conference, 1995.
[PDF]
[PDF]
Hybrid Decision Diagram: Overcoming the Limitation of MTBDDs and BMDs
Clarke, E.M., Fujita, M., & Zhao, X.
Proceedings of International Conference on Computer-Aided Design (ICCAD '95), pp. 159-163, 1995.
[PDF]
[PS]
Automatic Verification of Industrial Designs
Hartonas-Garmhausen, V., Kurfess, T., Clarke, E.M., & Long, D.
Proceedings: Workshop on Industrial Strength Formal Specification Techniques, pp.88-96, 1995.
[PDF]
Verifying the Performance of the PCI Local Bus Using Symbolic Techniques
Campos, S., Clarke, E.M., Marrero, W., & Minea, M.
International Conference on Computer Design, October 1995.
[PDF]
[Tech. Report]
Verifying Parametrized Networks using Abstraction and Regular Languages
Clarke, E.M., Grumberg, O., & Jha, S.
6th International Conference on Concurrency Theory, CONCUR '95, Philadelphia, PA, August 1995, pp. 395-407.
[PS]
Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking
Clarke, E.M., Grumberg, O., McMillan, K.L., & Zhao, X. Design
Automation Conference (DAC ’95), San Francisco, CA, June 1995.
[PDF]
Verus: A Tool for Quantitative Anaylsis of Finite-State Real-Time Systems
Clarke, E.M., Campos, S., Marrero, W., & Minea, M.
Workshop on Languages, Compilers and Tools for Real-Time Systems, La Jolla, Ca, June, 1995.
[PS]
Timing Analysis of Industrial Real-Time Systems
Campos, S., Clarke, E., Marrero, W., & Minea, M.
Proceedings of the Workshop on Industrial Strength Formal Specification Techniques, pp. 97-107, April 1995.
[PDF]
Computing Quantitative Characteristics of Finite-State Real-Time Systems
Campos, S., Clarke, E. M., Marrero, W., Minea M., Hiraishi, H.
IEEE Real-Time Systems Symposium, Puerto Rico, December, 1994.
[PDF]
Automatic Verification of Finite-state Concurrent Systems.
Edmund M. Clarke:
Application and Theory of Petri Nets 1994: 1
[PDF]
Automatic Verification of Finite-State Concurrent Systems.
Edmund M. Clarke:
LICS 1994: 126
[PDF]
Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan
Clarke, E.M., and Zhao, X.
12th International Conference on Automated Deduction, Nancy, France, June/July 1994. Lecture Notes in Artificial Intelligence 814, A. Bundy (Ed.), pp. 758-763.
[PDF]
[PS]
An Improved Algorithm for the Evaluation of Fixpoint Expressions
Clarke, E.M., Long, D., Browne, A., Jha, S., & Marrero, W.
Conference on Computer-Aided Verification, Stanford CA, June 21-23,1994. Springer Lecture Notes in Computer Science, 818, Dill D. (Ed.), pp. 338-351.
[PDF]
[PDF]
[PDF]
[PS]
Another Look at LTL Model Checking
Clarke, E.M., Grumberg, O., and Hamaguchi, K.
Conference on Computer-Aided Verification, Stanford, CA, June 21-23, 1994. Springer Lecture Notes in Computer Science 818, D. Dill (Ed.), pp.415-428.
[PDF]
[PS]
Fast Spectrum Computation for Logic Functions using Binary Decision Diagrams
Fujita, M., Chih-Yuan Yang, J., Clarke, E.M., Zhao, Z., & McGeer,P.
Proceedings: IEEE International Symposium on Circuits and Systems ISCAS '94, 1994.
[PDF]
Real-Time Symbolic Model Checking for Discrete Time Models
Clarke, E.M., and Campos, S.
First AMAST International Workshop in Real-Time Systems, Iowa City, IA, November 1-3, 1993.
[PS]
Efficient Verification of Parallel Real-Time Systems
Clarke, E.M., Yoneda, T., Shibayama, A., and Schlingloff, H.
Conference on Computer-Aided Verification, Heraklion, Crete, Greece, June 28-July 1, 1993. Springer Lecture Notes in Computer Science 697, C. Courcoubetis (Ed.), pp. 321-332.
[PS]
Exploiting Symmetry in Temporal Logic Model Checking
Clarke, E.M., Filkorn, T. and Jha, S.
Conference on Computer-Aided Verification, Heraklion, Crete, Greece, June 28-July 1, 1993. Springer Lecture Notes in Computer Science 697, C. Courcoubetis (Ed.), pp. 450-463.
[PDF]
Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping
Clarke, E.M., McMillan, K.L., Zhao, X., Fujita, M. and Yang, J.
30th ACM/IEEE Design Automation Conference, Dallas, TX, June 14-18, 1993.
[PDF]
Automatic Verification of Sequential Circuit Designs.
Edmund M. Clarke:
CHDL 1993: 165
[PDF]
Verification Tools for Finite-State Concurrent Systems.
Edmund M. Clarke, Orna Grumberg, David E. Long:
REX School/Symposium 1993: 124-175
[PDF]
Verification of the Futurebus + Cache Coherence Protocol
Clarke, E.M., Grumberg, O., Hiraishi, H., Jha, S., Long, D.E., McMillan, K.L., and Ness, L.A.
CHDL '93: The IFIP Conference on Hardware Description Langauges and their Applications, Ottawa, Canada, April 26-28, 1993.
[PDF]
[PS]
Model Checking and Abstraction
Clarke, E.M., Grumberg, O., and Long, D.E.
The 19th ACM Symposium on Principles of Programming Languages, Albuquerque, NM, January 1992.
[PDF]
[PS]
Analytica - A Theorem Prover in Mathematica.
Edmund M. Clarke, Xudong Zhao:
CADE 1992: 761-765
[PDF]
[longer version]
Representing Circuits More Efficiently in Symbolic Model Checking
Burch, J.R., Clarke, E.M., & Long, D.E.
28th ACM/IEEE Design Automation Conference, pp. 403-407, 1991.
[PDF]
Symbolic Model Checking with Partitioned Transition Relations
Clarke, E.M., Burch, J.R., & Long, D.E.
VLSI 91, Edinburgh Scotland, August 1991. Winner of the Sidney Michaelson Best Paper Award.
[PDF]
[Tech. Report]
Parallel Symbolic Computation on Shared Memory Multiprocessor
Clarke, E.M., Kimura, S., Long, D.E., Michaylov, S., Schwab, S.A., and Vidal, J.P.
International Symposium on Shared Memory Multiprocessors, Tokyo, Japan, April 1991.
[PDF]
A Unified Approach for Showing Language Containment and Equivalence between Various Types of Automata
Clarke, E.M., Draghicescu, I.A., & Kurshan, R.P.
15th Colloquium on Trees in Algebra and Programming, Copenhagen Denmark, May 1990 (Springer LNCS 431).
[PDF]
Symbolic Model Checking: 10^20 States and Beyond
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., & Hwang, L.J.
Proceedings: Fifth Annual IEEE Symposium Logic in Computer Science, 1990.
[PDF]
Sequential Circuit Verification Using Symbolic Model Checking
Burch, J.R., Clarke, E.M., McMillan, K.L., & Dill, D.L.
Proceedings: 27th Design Automation Conference, 1990.
[PDF]
A Parallel Algorithm for Constructing Binary Decision Diagrams
(1st is accurate copy but more slanted than 2nd copy)
Kimura, S. and Clarke, E.M.
Proceedings: IEEE International Conference on Computer Design: VLSI in Computers and Processors, 1990.
[PDF]
[PDF]

Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem.
Edmund M. Clarke:
CAV 1990: 1
[PDF]
A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems
Clarke, E.M., Grumberg, O., and Kurshan, R.P.
Logic at BOTIC '89: Seminar on Logical Foundations of Computer Science, Pereslavl-Zalessky, USSR, July 2-9, 1989. Springer Lecture Notes in Computer Science 363, A.R. Meyer and M.A. Taitslin (Eds.), pp. 81-90.
[PDF]
A Language for Compositional Specification and Verification of Finite State Hardware Controllers
Clarke, E.M., Long, D.E., & McMillan, K.L.
Ninth International Symposium on Computer Hardware Description Languages and their Applications, Washington, DC, June 19-21, 1989.
[PS]
Parthenon: A Parallel Theorem Prover for Non-horn Clauses
Bose, S., Clarke, E.M., Long, D.E., & Michaylov, S.
Proceedings: 4th Annual Symposium on Logic in Computer Science (LICS '89), pp.80-89, 1989.
[PDF]
[PDF]
Compositional Model Checking
Clarke, E.M., Long, D.E., & McMillan, K.L.
Proceedings: 4th Annual Symposium on Logic in Computer Science (LICS '89), pp.353-362, 1989.
[PDF]
[PS]
PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses.
P. E. Allen, Soumitra Bose, Edmund M. Clarke, Spiro Michaylov:
CADE 1988: 764-765
[PDF]
Avoiding the State Explosion Problem in Temporal Logic Model Checking Algorithms
Clarke, E.M., and Grumberg, O.
1987 ACM Symposium on Principles of Distributed Computing, Vancouver, Canada., 1987.
[PDF]
Characterizing Kripke Structures in Temporal Logic
Clarke, E.M., Browne, M.C. and Grumberg, O. 1987 TAPSOFT Conference, Pisa, Italy.
[PDF]
Reasoning about Networks with Many Identical Processes
Clarke, E.M., Browne, M. and Grumberg, O.
1986 ACM Symposium on Principles of Distributed Computing, Calgary, Canada, 1986.
[PDF]
True Relative Completeness of an Axiom System for the Language L4 (Abridged).
Steven M. German, Edmund M. Clarke, Joseph Y. Halpern:
LICS 1986: 11-25
Escher-A Geometrical Layout System for Recursively Defined Circuits
Clarke, E.M. and Feng, Y.
23rd ACM/IEEE Design Automation Conference, Las Vegas NV, June 29-July 2 1986.
[PDF]
Checking the Correctness of Sequential Circuits
Clarke, E.M., Browne, M.C., & Dill, D.
1985 IEEE International Conference on Computer Design: VLSI in Computers, Rye Towne Hilton, Rye Brook, N.Y., pp. 545-548, October 7-10, 1985.
Automatic Verification of Sequential Circuits using Temporal Logic
Clarke, E.M., Browne, M., Dill, D., and Mishra, B.
7th International Conference on Computer Hardware Description Languages, Tokyo, Japan, August 29-31, 1985. Edited by C.J. Koomen and T. Moto-oka.
[PDF]
Automatic Verification of Asynchronous Circuits Using Temporal Logic
Clarke, E.M., and Dill, D.
IFIP WG 10.2/10.5 Workshop on Hardware Design Verification, Technical University of Darmstadt, Fed. Rep. of Germany, November 26-27, 1984. Also, Proceedings of the 1985 Chapel Hill Conference on VLSI, University of North Carolina at Chapel Hill, NC, May 15-17, 1985.
[PDF]
Compiling Path Expressions into VLSI Circuits
Clarke, E.M., Anatharaman, T.S., Foster, M.J., & Mishra, B.
12th Annual ACM Symposium on Principles of Programming Languages, New Orleans, LA, January 14-16, 1985.
[PDF]
A Methodology for Verifying Request Processing Protocols
Clarke, E.M., Nikolaou, C.N., Francez, N. and Schuman, S.
ACM SIGCOMM 83 Symposium on Communications, Architecture, and Protocols, Austin, TX, March 8-9, l983.
[PDF]
Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach
Clarke, E.M., Emerson, E.A. and Sistla, A.P.
Tenth ACM Symposium on Principles of Programming Languages, Austin, TX, January 24-26, l983.
[PDF]
[PDF]
The Complexity of Propositional Linear Temporal Logic
Sistla, A.P. and Clarke, E.M.
Proceedings: Fourteenth Annual ACM Symposium on Theory of Computing, 1982.
[PDF]
Can Message Buffers be Characterized in Linear Temporal Logic?
Clarke, E.M., Sistla, A.P., Francez, N., and Gurerich, Y.
ACM Sigact-Sigops Symposium on Principles of Distributed Computing, Ottawa, Canada, August l8-20, l982.
[PDF]
On Effective Axiomatizations of Hoare Logics
Clarke, E.M., German, S.M., & Halpern, J.Y.
Ninth Annual Symposium on Principles of Programming Languages, 1983.
[PDF]
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic.
Edmund M. Clarke, E. Allen Emerson:
Logic of Programs 1981: 52-71
[PDF]
Programming Distributed Applications in ADA: A First Approach
Clarke, E.M., Schuman, S.A., and Nikolaou, C.N.
Tenth Annual International Conference on Parallel Programming, Bellaire, MI, August 25, 1981.
[PDF]
Reconfiguration Strategies for Reliable Shared Memory Multiprocessor Systems
Clarke, E.M., and Nikolaou, C.N.
11th International Symposium on Fault-Tolerant Computing, Portland, ME, June 25, 1981.
[PDF]
Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data
Clarke, E.M., Bernstein P.A., & Blaustein, B.T.
6th International Conference on Very Large Data Bases, Montreal, Canada, October 1980.
[PDF]
Characterizing Correctness Properties of Parallel Programs Using Fixpoints
Clarke, E.M. and Emerson, A.
ICALP80, Noordwijkerhout, Netherlands, July 1980. In Springer Lecture Notes in Computer Science 85, Springer-Verlag, pp. 169-181.
[PDF]
Approximate Algorithms for Optimization of Busy Waiting in Parallel Programs
Clarke, E.M. and Liu, L.
20th FOCS, San Juan, PR, October 1979.
[PDF]
Synthesis of Resource Invariants for Concurrent Programs
Clarke, E.M.
Proceedings: Sixth ACM Symposium on Principles of Programming Languages, 1979.
[PDF]
Program Invariants as Fixed Points
Clarke, E.M.
Proceedings: 18th Annual Symposium on Foundations of Computer Science, Providence, RI, October 31-November 2, 1977.
[PDF]
Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems
Clarke, E.M.
Proceedings: 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, 1977.
[PDF]
[Tech. Report]
[Extended T.R.]

Top

Invited Journal Articles

PDF format

Other formats

Counterexample Guided Abstraction Refinement
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., and Veith, H.
Submitted to Journal of the ACM.
[PS]
Verification of Out-of-Order Processor Designs Using Model Checking and Light-Weight Completion Function
Clarke, E.M., Berezin, S., Biere, A., and Zhu, Y.
Formal Methods in Ststem Design, Vol. 20, No. 1, pp. 152-186, 2002.
[PDF]
State Space Reduction Using Partial Order Techniques
Clarke, E.M., Minea, M., Grumberg, O., and Peled, D.
Software Tools for Technology Transfer, Vol. 3, No. 1, pp. 279-287, 1999.
[PDF]
Compositional Reasoning in Model Checking
Clarke, E.M., Berezin, S., and Campos, S.
Lecture Notes in Computer Science 1536, pp. 81-103, 1998.
[PDF]
Formal Methods: State of the Art and Future Directions
Clarke, E.M. and Wing, J.M.
ACM Computing Surveys, December 1996. Also available as CMU-CS-96-178.
[PDF]
[PS]
Automatic Verification of Sequential Circuit Designs
Clarke, E.M., Burch, J.R., Grumberg, O., Long, D.E.,and McMillan, K.L.
Phil. Trans. R. Soc. Lond. A., 339, 1992, pp.105-109.
[PDF]
A Language for Compositional Specification and Verification of Finite State Hardware Controllers
Clarke, E.M., Long, D.E, & McMillan, K.L.
Proceedings: IEEE , Vol. 79, No. 9, pp. 1283 -1292, 1991.
[PDF]
[PS]
Research On Automatic Verification of Finite-State Concurrent Systems
Clarke, E.M., and Grumberg, O.
Annual Reviews of Computer Science, No. 2, pp. 269-90, 1987.
[PDF]
Introduction to Special Issue on Distributed Computing Issues in Hardware Design
Clarke, E.M.
Distibuted Computing, Vol. 1, No. 4, 1986.
The Characterization Problem for Hoare Logics
Clarke, E.M.
Phil. Trans. R. Soc. Lond. A 312, 1984, pp.423-440.
[PDF]

Top

Invited Conference Articles

PDF format

Other formats

Model Checking: Historical Perspective and Example
Clarke, E.M., and Berezin, S.
Proceedings of Analytic Tableaux and Related Methods (TABLEAU ’98) Oisterwijk near Tilburg, The Netherlands, no. 1397, pp. 18-24, May 4-7, 1998.
[PDF]
Model Checking
Clarke, E.M., Grumberg, O., & Long, D. Proceedings:
International Summer School on Deductive Program Design, 1994. Springer-Verlag Nato Asi, Series F, Vol. 152, 1996.
[PDF]
Verification Tools for Finite-State Concurrent Systems
Clarke, E.M. REX
'93 School/ Workshop: 'A Decade of Concurrency'. Noordwijkerhout, The Netherlands, June 1-4, 1993. Springer Lecture Notes in Computer Science, No. 684, pp. 124-175, 1994.
[PDF]
Expressibility Results for Linear-time and Branching-time Logics
Clarke, E.M. and Draghicescu, A.I.
REX Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Noordwijkerhout, The Netherlands, May 30-June 3, 1988. Springer Lecture Notes in Computer Science, No. 354, pp. 428-438.
[PDF]
The Design and Verification of Finite State Hardware Controllers
Clarke, E.M., Bose, S., Browne, M.C. and Grumberg, O.
1987 International Symposium on VLSI Technology, Systems and Applications, pp. 53-61, Taipei, Taiwan, May 1987.
[PDF]
The Model Checking Problem for Concurrent Systems with Similar Processes
Clarke, E.M., and Grumberg, O.
Colloquium on Temporal Logic and Specification, Altrincham, Cheshire, Sponsored by Alvey/SERC, April, 1987. In Temporal Logic in Specification, B. Banieqbal, H. Barringer, A. Pnueli (Eds.), Springer Lecture Notes in Computer Science, No. 398, pp. 188-202.
[PDF]
Automatic Verification of Asynchronous Circuits
Clarke, E.M., and Mishra, B.
Logics of Programs 1983, Springer Lecture Notes in Computer Science, No.164, Springer Verlag, 1984.
[PDF]
Reasoning About Procedures as Parameters
Clarke, E.M., German, S.M., and Halpern, J.Y.
Logics of Programs 1983, Springer Lecture Notes in Computer Science, No. 164, Springer Verlag 1984.
[PDF]
Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic
Clarke, E.M., and Emerson, E.A.
Logics of Programs 1981, Springer Lecture Notes in Computer Science, No. 131, Springer-Verlag, 1982.
[PDF]

Top

Technical Reports, Unpublished Manuscripts, Papers Appearing in Unreferred Conferences and Workshops

PDF format

Other formats

Revisiting the Complexity of Stability of Continuous and Hybrid Systems.
Sicun Gao, Soonho Kong, Edmund M. Clarke:
CoRR abs/1404.7169 (2014)
[PDF]
Delta-Complete Analysis for Bounded Reachability of Hybrid Systems.
Sicun Gao, Soonho Kong, Wei Chen, Edmund M. Clarke
CoRR abs/1404.7171 (2014)
[PDF]
SReach: Combining Statistical Tests and Bounded Model Checking for Nonlinear Hybrid Systems with Parametric Uncertainty.
Qinsi Wang, Paolo Zuliani, Soonho Kong, Sicun Gao, Edmund M. Clarke:
CoRR abs/1404.7206 (2014)
[PDF]
Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions.
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke
CoRR abs/1407.1524 (2014)
[PDF]
Proof Generation from Delta-Decisions.
Sicun Gao, Soonho Kong, Edmund M. Clarke
CoRR abs/1409.6414 (2014)
[PDF]
Towards Personalized Cancer Therapy Using Delta-Reachability Analysis.
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke
CoRR abs/1410.7346 (2014)
[PDF]
Verifying Fault Tolerant Real-Time Buses
Clarke, E.M.
Workshop on Embedded Computing, Atlanta, Georgia, Nov. 15-16, 2001.
Using Cutwidth to Improve Sumbolic Simuation and Boolean Satisfiability
Wang, D., Clarke, E., Zhu, Y., & Kukula, J.
Proceedings: High-Level Design Validation and Test Workshop, 2001.
[PS]
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking
Clarke, E.M., Williams, P.F., Biere, A., and Gupta, A.
TechCon '00, Phoenix, Arizona, September 2000.
[PDF]
[PS]
EPSL: Executable Protocol Specification Language (Short paper)
Clarke, E.M., Wang, D., Lu, Y., and Veith, H.
Symposium on Logics in Computer Science (LICS '00), Santa Barbara, CA., June 26-29 2000.
[PDF]
Counterexample-Guided Abstraction Refinement
Clarke, E.M., Grumber, O., Jha, S., Lu, Y., and Veith, H.
Carnegie Mellon University, Computer Science Department, Technical Report, CMU-CS-00-103, 2000.
[PDF]
[PS]
[PS]
Program Slicing of Hardware Description Languages
Clarke, E.M., Fujita, M., Rajan, S.P., Reps, T., Shankar, S., and Teitelbaum, T.
Carnegie Mellon University, Computer Science Department, Technical Report, CMU-CS-99-103, 1999.
[PDF]
Combining Local and Global Model Checking
Clarke, E.M., Biere, A. and Zhu, Y. University of Karlsruhe,
Technical Report 26/98, (extended Version of the SMC ’99 Paper), 1998.
[PDF]
[PS]
Hybrid Spectral Transform Diagrams
Clarke, E.M., Fujita, M., and Heinle, W.
Carnegie Mellon University, Computer Science Department, Technical Report, CMU-CS-97-149, 1997.
[PDF]
[PS]
Word Level Symbolic Model Checking A New Approach for Verifying Arithmetic Circuits
Clarke, E.M.and Zhao, X.
Carnegie Mellon University, Computer Science Department, Technical Report, CMU-CS-95-161, 1995.
[PDF]
Application of Multi-Terminal Binary Decision Diagrams
Clarke, E.M., Fujita, M., and Zhao, X.
Carnegie Mellon University, Computer Science Department, Technical Report, CMU-CS-95-160, 1995.
[PDF]
Computing Quantitative Characteristics of Finite-State Real-Time Systems
Campos, S., Clarke, E.M., Marrero, W., Minea, M., Hiraishi, H.
Carnegie Mellon University, Computer Science Department, Technical Report, CMU-CS-94-147, 1994.
[PDF]
A VHDL Subset for model-checking
Clarke, E.M.
Carnegie Mellon University, Computer Science Department, 1994.
[PDF]
Multi-Terminal Binary Decision Diagrams: An Efficient Data Structure for Matrix Representation
Clarke, E.M., Fujita, M., McGeer, P., Yang, J., and Zhao, X.
IWLS '93 International Workshop on Logic Synthesis, Tahoe City, CA, May 23-26 1993.
[PDF]
Multi-Terminal Binary Decision Diagrams and Hybrid Diagrams
Clarke, E.M., Fujita, M., and Zhao, X.
1993.
[PDF]
Analytica-An Experiment in Combining Theorem Proving and Symbolic Computation
Clarke, E.M. and Zhao, X.
Carnegie Mellon University, Computer Science Department, Technical Report, CMU-CS-92-147, October 1992.
[PS]
Parthenon: A Parallel Theorem Prover for Non-horn Clauses
Bose, S., Clarke, E.M., Long, D.E., and Michaylov, S.
System Abstracts, Ninth International Conference on Automated Deduction, Springer Lecture Notes in Computer Science, 310, pp.764-5.
[PDF]
[PDF]
CSML Language Reference
Browne, M., Clarke, E.M., and McMillan, K.L.
Carnegie Mellon University, Computer Science Department, May 10, 1989
[PDF]
The Design and Verification of Finite State Hardware Controllers
Clarke, E.M. Bose, S., Browne, M., and Grumberg, O.
Research Review, Carnegie Mellon University, Computer Science Department, pp.53-61, 1986/1987.
[PDF]
Automatic and Hierarchical Verification of Asynchronous Circuits Using Temporal Logic
Mishra, B., and Clarke, E.M.
Carnegie Mellon Univeristy, Computer Science Department, CMU-CS-83-155, l983.
[PDF]
ADAPT: ADA Distributed Application Prototyping Technique
Clarke, E.M., Sattley, J., Sattley, K., Schaffner, S., and Schuman, S.
ACM SIGSOFT Software Engineering Symposium: Rapid Prototyping, Columbia, MD, April 19-21, l982.
[PDF]
A Proof Methodology For Verifying Request Processing Protocols
Nikolaou, C.N., Clarke, E.M., Shuman, S.A.
Harvard University, TR-04-82, January, l982.
[PDF]
Research Directions in Programming Language Semantics and Formal Program Verification
Clarke, E.M.
Harvard University, Center for Research in Computing Technology, Technical Report, TR-22-81, September l981.
[PDF]
Programming Distributed Applications in ADA: A First Approach
Clarke, E.M., Schuman, S.A., and Nikolaou, C.N.
Massachusetts Computer Associates Report CADD-8l03-3l02, March 3l, l98l.
Optimization of Busy Waiting in Conditional Critical Regions
Clarke, E.M., and Liu, L.
13th Hawaii International Conference on System Sciences, Honolulu, HI, January 1980.
[PDF]
Characterizing Correctness Properties of Parallel Programs Using Fixpoints
Emerson, E.A., Clarke, E.M.
TR-04-80, April, 1980.
[PDF]
The Impact of Multiprocessor Technology on High Level Language Design
Clarke, E.M., Evans, A., Morgan, R., and Roberts, E.
BBN Report 4188, September 1979.
A Summary of Research on Program Derivation
Clarke, E.M.
Duke University, Department of Computer Science, Technical Report, CS-1978-9, October 1978.
[PDF]
Concurrent Programs are Easier to Verify Than Sequential Programs
Clarke, E.M.
Duke University, Department of Computer Science, Technical Report, CS-1978-6, July 1978. Also presented at the NSF-SBMS Conference on Logic of Computer Programming, held at Renssaelaer Polytechnic Institute, Troy, NY, June 1978.
[PDF]
Proving Coroutines Without History Variables
Clarke, E.M.
Proceedings: 16th Annual Southeast Regional ACM Conference, 1978.
[PDF]
[PDF]
Hoare-axioms and the Semantics of Control Structures
Clarke, E.M.
Duke University, Department of Computer Science, Technical Report, CS-1977-10, November 1977.
[PDF]
Pathological Interaction of Programming Language Features
Clarke, E.M.
Duke University, Department of Computer Science, Technical ReportCS-1976-15, October 1976. Also presented at the North Carolina Workshop on Control Structures Held at North Carolina State University, March 17-18, 1977.
[PDF]

Top

Books and Edited Volumes

PDF format

Other formats

Model Checking, Second Edition
Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. MIT Press, 2018.
Bounded Model Checking.
Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Y. Zue:
Book chapter: Advances in Computers, Academic Press, 2003.
[PDF]
Model Checking
Edmund M. Clarke, Bernd-Holger Schlingloff:
Handbook of Automated Reasoning 2001: 1635-1790
[PS]
Model Checking
Clarke, E.M., Grumberg, O. and Long, D.

[PDF]

Model Checking
Clarke, E.M., Grumberg, O., and Peled, D. MIT Press, 2000.
Clarke, E.M., and Kurshan, R.P.
Proceedings of the Second Workshop on Computer-Aided Verification, Springer Lecture Notes in Computer Science 531, Springer-Verlag, 1991.
Clarke, E.M., and Kozen, D.
Proceedings of the 1983 Workshop on Logics of Programs, Springer Lecture Notes in Computer Science 164, Springer-Verlag, 1984.

Top

Contributions to Edited Volumes

PDF format

Other formats

Parameter Synthesis for Cardiac Cell Hybrid Models Using d-Decisions
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani, Edmund M. Clarke:
CMSB 2014: 99-113, 2014
[PDF]
Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems with Application to Patient-Specific Cardiac Dynamics and Devices.
Radu Grosu, Elizabeth Cherry, Edmund M. Clarke, Rance Cleaveland, Sanjay Dixit, Flavio H. Fenton, Sicun Gao, James Glimm, Richard A. Gray, Rahul Mangharam, Arnab Ray, Scott A. Smolka:
ISoLA (2) 2014: 356-364, 2014
[PDF]
Model Checking Hybrid Systems - (Invited Talk).
Clarke, E.M., Gao, S.
ISoLA (2) 2014: 385-386, 2014
[PDF]
Progress on the State Explosion Problem in Model Checking
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., and Veith, H.
Informatics - 10 Years Back, 10 Years Ahead (LNCS '00), Springer Verlag, pp. 176-194, 2000.
[PS]
Representations of Discrete Functions
Clarke, E.M., Fujita, M., and Zhao, X. Tsutomu Sasao and Masahiro Fujita (Eds.),
Kluwer Academic Publishers, pp. 93-108, 1996.
[Chapter]
[Book]
Real-Time Symbolic Model Checking for Discrete Time Models
Clarke, E.M. and Campos, S. In T. Rus and C. Rattray (Eds.),
AMAST Series in Computing Theories and Experiences for Real-Time System Development, World Scientific Publishing Company, 1995.
[PDF]
[PS]
Parallel Symbolic Computation on Shared Memory Multiprocessor
Clarke, E.M., Kimura, S., Long, D.E., Michaylov, S., Schwab, S.A., and Vidal, J.P. In Norihisa Suzuki (Ed.),
Proceedings of the First International Conference on Shared Memory Multiprocessors, MIT Press, pp. 53-81, 1992.
[PDF]
A Language for Compositional Specification and Verification of Finite State Hardware Controllers
Clarke, E.M., Long, D.E., & McMillan, K.L.
Formal Verification of Hardware Designs, Michael Yoeli (Ed.), IEEE
[PDF]
Sequential Circuit Verification Using Symbolic Model Checking
Burch, J.R., Clarke, E.M., McMillan, K.L., & Dill, D.L.
Frontiers in Formal Methods Applied to Hardware Design, Springer Verlag, pp. 46-51, 1990.
[PDF]
SML - A High Level Language for the Design and Verification of Finite State Machines
Clarke, E.M. and Browne, M.C. In D. Borrione (Ed.),
From HDL Descriptions to Guaranteed Correct Circuit Designs, North Holland, 1987.
[PDF]
Compiling Path Expressions into VLSI Circuits
Anantharaman, T.S., Clarke, E.M., Foster, M.J., & Mishra, B. In Yechiam Yemini (Ed.),
Current Advances In Distributed Computing And Communications, Computer Science Press, 1987. Reprinted from Distributed Computing, 1986.
[PDF]
Automatic Verification of Sequential Circuits Using Temporal Logic
Clarke, E.M., Browne, M.C., Dill, D.L. and Mishra, B. In Michael Yoeli (Ed.),
Formal Verification of Hardware Designs, IEEE Computer Society Press Tutorial, pp. 166-175, 1991. Reprinted from IEEE Transactions on Computers, 1986.
[PDF]
Automatic Verification of Asynchronous Circuits Using Temporal Logic
Clarke, E.M. and Dill, D.L.
In Michael Yoeli (Ed.), Formal Verification of Hardware Designs, IEEE Computer Society Press Tutorial, pp. 176-182, 1991. Reprinted from IEEE Proceedings, 1986.
[PDF]
[PDF]
Automatic Circuit Verification Using Temporal Logic: Two New Examples
Clarke, E.M., Browne, M.C., & Dill, D.L.
In G.J., Milne and P.A. Subrahmanyam (Eds.), Formal Aspects of VLSI Design, Elsevier Science Publishers, North Holland, 1986.
[PDF]
Using Temporal Logic for the Automatic Verification of Finite State Systems
Clarke, E.M., Browne, M., Emerson, A., & Sistla, P.
In Krzysztof R. Apt (Ed.), Logic and Models for Concurrent Systems, Springer-Verlag, 1985.
[PDF]
The Characterization Problem for Hoare Logics
Clarke, E.M. In C.A.R. Hoare and J.C. Shepherdson (Eds.), Mathematical Logic and Programming Languages, Prentice-Hall International Series in Computer Science, 1984. Reprinted from Phil. Trans. R. Soc. Lond. A, 312, pp. 423-440, 1984.
[PDF]
A Critical Evaluation of ADA for Multiprocessor Systems
Clarke, E.M., Evans, A., Morgan, R., and Roberts, E.
In Narain Gehani and Andrew D. McGettrick (Eds.), Concurrent Programming, International Computer Science Series, Addison-Wesley, pp. 436-475. Reprinted from Software Practice and Experience, 1981.