Technical Reports, Unpublished Manuscripts, Papers Appearing in Unreferred Conferences and Workshops
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 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 Axioms
| 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. |