Thesis |
PDF format |
| Completeness and Incompleteness Theorems for Hoare-Like Axiom Systems (Sept 1976) | [PDF] |
Papers Published in Refereed Journals |
PDF format |
Other formats |
|
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) |
|
|
|
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. |
|
|
|
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. |
|
|
|
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. |
|
|
|
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) |
|
|
| Formal Methods: State of the Art and Future Directions
Clarke, E.M. and Wing, Jeannette |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
||
| 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. |
|
|
| 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. |
|
|
| State
Space Reduction Using Partial Order Techniques Clarke, E.M., Grumberg, O., Minea, M., Peled, D. 1998 |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
||
| 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. |
|
|
| 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. |
|
|
| Computer-Aided Verification
Clarke, E.M. & Kurshan, R.P. IEEE Spectrum, Vol. 33 (6), pp. 61-67, June 1996. |
||
| 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. |
|
|
| 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. |
|
|
| Model Checking and Abstraction
Clarke, E.M., Grumberg, O., & Long, D.E. ACM TOPLAS, Vol. 16, No. 5, pp. 1512-1542, September 1994. |
|
|
|
Symbolic Model Checking for Sequential Circuit
Verification |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| Reasoning about Networks with Many Identical Processes
(Problem is this is 86 version but specs is 89) Clarke, E.M., Browne, M., & Grumberg, O. Information and Computation, Vol. 81, No. 1, pp. 13-31, April 1989. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
|
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. |
|
|
| Hierarchical Verification of Asynchonous Circuits Using Temporal Logic
Clarke, E.M. and Mishra, B. Theoretical Computer Science. Vol. 38, pp. 269-291, 1985. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons
Clarke, E.M. and Emerson, E.A. Science of Computing 2, pp. 241-266, 1982. |
|
|
| 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. |
|
|
| A Critical Evaluation of ADA for Multiprocessor Systems
Clarke, E.M., Evans, A., Morgan, R., & Roberts. E. Software: Practice and Experience, Vol. 11, pp. 1019-1051, 1981. |
|
|
| Proving the Correctness of Coroutines Without History Variables
Clarke, E.M.Acta Informatica, Vol.13, pp. 169-188, 1980. |
|
|
| Synthesis of Resource Invariants for Concurrent Programs
Clarke, E.M. ACM TOPLAS, Vol. 2, No. 3, pp. 338-358, July 1980. |
|
|
| Program Invariants as Fixed Points
Clarke, E.M. Computing, Vol. 21, No.4, pp. 273-294, 1979. |
|
|
| 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. |
|
Papers Presented at Refereed Conferences and Workshops |
PDF format |
Other formats |
|
Completeness and complexity of bounded model checking. Edmund M. Clarke, Daniel Kroening, Joel Ouaknine, Ofer Strichman: VMCAI 2004, LNCS (to appear). |
[PS] | |
|
Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang CAV 2003: 126-140 |
|
|
|
Behavioral consistency of C and verilog programs using bounded model checking Edmund M. Clarke, Daniel Kroening, Karen Yorav: DAC 2003: 368-371 |
|
|
|
Modular Verification of Software Components in C. Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith: ICSE 2003: 385-395 |
|
|
|
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 |
|
|
|
State/event-based software model checking. Edmund M. Clarke, Joel Ouaknine, Natasha Sharygina, Nishant Sinha: Submitted to IFM 2003. |
|
|
|
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). |
|
|
|
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). |
[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. |
|
|
| 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. |
|
|
| 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. |
|
|
|
A 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 |
||
| 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. |
|
|
|
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. |
||
| 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 (ICSE ’01), 2001. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| Efficient Variable Ordering Using a BDD Based Sampling Scheme
Lu. Y,. Jain, J., Clarke, E. & Fujita, M. Proceedings: Design Automation Conference (DAC ’00), 2000. |
|
|
| 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. |
|
|
| 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. |
|
|
|
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. |
|
|
|
Improving BDD Variable Ordering Using Abstract BDDs and Sampling
Proceedings of International Workshop of High Level Design, Verification and Testing, (HLDVT), San Diego, California November 4-6 1999. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
|
Verifying IP-Core Based System-On-Chip Design
12th Annual IEEE International ASIC/SOC Conference, pp. 27-31, 1999. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
|
Symbolic Model Checking Without BDDs
Lecture Notes in Computer Science, Proceedings: Tools and Algorithms for Construction and Analysis of Systems (TACAS ’99), No. 1579, pp. 193-207, 1999. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| NuSMV: A reimplementation of SMV
Clarke, E.M., Cimatti, A., Giunchiglia, F., & Roveri, M. Proceedings: 1st Feature Integration in Requirements Engeering (FIREworks '98), 1998. |
|
|
| 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. |
|
|
|
Using State Space Exploration and a Natural Deduction Style Message Derivation Engine to Verify Security Protocols
Proceedings of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET),Shelter Island, New York, pp. 96-106, 1998 |
|
|
|
On the Semantic Foundations of Probabilistic VERUS
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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
|
The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems
Computer Aided Verification 9th International conference (CAV ’97). Haifa, Israel, Vol. 1254, June, 1997. |
|
|
|
Model Checking for Security Protocols Marrero, W., Clarke, E.M., Jha,S.
|
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
|
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. |
|
|
| 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. |
|
|
| 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. |
|
|
| Formally Verifying Arithmetic Circuits - Avoiding the Pentium FDIV Bug
Clarke, E.M. Intel Design and Test Technology Conference, 1995. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
|
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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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). |
|
|
| Symbolic Model Checking: 1020 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| Parthenon: A Parallel Theorem Prover for Non-horn Clauses
(1st version is slightly slanted but is the more accurate version than 2nd paper) 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| Characterizing Kripke Structures in Temporal Logic Clarke, E.M., Browne, M.C. and Grumberg, O. 1987 TAPSOFT Conference, Pisa, Italy. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
|
Compiling Path Expressions into VLSI Circuits Clarke, E.M., Anatharaman, T.S., Foster, M.J., & Mishra, B.
|
|
|
| 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. |
|
|
| 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. |
|
|
| The Complexity of Propositional Linear Temporal Logic
Sistla, A.P. and Clarke, E.M. Proceedings: Fourteenth Annual ACM Symposium on Theory of Computing, 1982. |
|
|
| 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. |
|
|
| On Effective Axiomatizations of Hoare Logics
Clarke, E.M., German, S.M., & Halpern, J.Y. Ninth Annual Symposium on Principles of Programming Languages, 1983. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| Approximate Algorithms for Optimization of Busy Waiting in Parallel Programs
Clarke, E.M. and Liu, L. 20th FOCS, San Juan, PR, October 1979. |
|
|
| Synthesis of Resource Invariants for Concurrent Programs
Clarke, E.M. Proceedings: Sixth ACM Symposium on Principles of Programming Languages, 1979. |
|
|
| Program Invariants as Fixed Points
Clarke, E.M. Proceedings: 18th Annual Symposium on Foundations of Computer Science, Providence, RI, October 31-November 2, 1977. |
|
|
| 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. |
|
|
Invited Journal Articles |
PDF format |
Other formats |
|
Counterexample Guided Abstraction Refinement Clarke, E.M., Grumberg, O., Jha,
S., Lu, Y., and Veith, H. |
||
| 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. |
||
| 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. |
|
|
| Compositional Reasoning in Model Checking
Clarke, E.M., Berezin, S., and Campos, S. Lecture Notes in Computer Science 1536, pp. 81-103, 1998. |
|
|
| 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. |
|
|
| 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. |
|
|
|
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. |
|
|
| 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. |
|
|
| 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. |
|
|
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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
Technical Reports, Unpublished Manuscripts, Papers Appearing in Unreferred Conferences and Workshops |
PDF format |
Other formats |
| 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. |
|
|
|
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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| Multi-Terminal Binary Decision Diagrams and Hybrid Diagrams
Clarke, E.M., Fujita, M., and Zhao, X. 1993. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| Proving Coroutines Without History Variables
Clarke, E.M. Proceedings: 16th Annual Southeast Regional ACM Conference, 1978. |
|
|
| Hoare-axioms and the Semantics of Control Structures
Clarke, E.M. Duke University, Department of Computer Science, Technical Report, CS-1977-10, November 1977. |
|
|
| 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. |
|
|
Books and Edited Volumes |
PDF format |
Other formats |
|
Bounded Model Checking. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Y. Zue: Book chapter: Advances in Computers, Academic Press, 2003. |
||
|
Model Checking. Edmund M. Clarke, Bernd-Holger Schlingloff: Handbook of Automated Reasoning 2001: 1635-1790 |
||
| Model Checking
Clarke, E.M., Grumberg, O. and Long, D. |
|
|
|
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. |
|
|
Contributions to Edited Volumes |
PDF format |
Other formats |
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
|
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 |
|
|
| 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. |
|
|
| 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. |
|
|
| 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. |
|
|
|
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. |
|
|
|
Automatic Verification of Asynchronous Circuits Using Temporal Logic Clarke, E.M. and Dill, D.L. |
||
|
Automatic Circuit Verification Using Temporal Logic: Two New Examples Clarke, E.M., Browne, M.C., & Dill, D.L. |
[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. |
|
|
| 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. |
|
|
| 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. |
|
|