Edmund M. Clarke
Affiliations:- Carnegie Mellon University, Pittsburgh, USA
According to our database1,
Edmund M. Clarke
authored at least 278 papers
between 1976 and 2018.
Collaborative distances:
Collaborative distances:
Awards
Turing Prize recipient
Turing Prize 2007, "For their roles in developing model checking into a highly effective verification technology, widely adopted in the hardware and software industries." awarded to Edmund M. Clarke and E. Allen Emerson and Joseph Sifakis.
ACM Fellow
ACM Fellow 1998, "Edmund M. Clarke is the co-inventor of Model Checking (with his former student Allen Emerson). He and his graduate students helped make Model Checking a tool that can be used to verify finite-state concurrent systems of industrial complexity.".
IEEE Fellow
IEEE Fellow 2005, "For contributions to model checking methods for formal verification.".
Timeline
Legend:
Book In proceedings Article PhD thesis Dataset OtherLinks
Online presence:
-
on zbmath.org
-
on scopus.com
-
on fi.edu
-
on viaf.org
-
on id.loc.gov
-
on d-nb.info
-
on cs.cmu.edu
-
on isni.org
-
on dl.acm.org
On csauthors.net:
Bibliography
2018
2017
Formal Methods Syst. Des., 2017
2016
Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 2016
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2016
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2016
Probabilistic reachability analysis of the tap withdrawal circuit in caenorhabditis elegans.
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2016
Proceedings of the Computational Methods in Systems Biology, 2016
Proceedings of the Computational Methods in Systems Biology, 2016
CyberCardia project: Modeling, verification and validation of implantable cardiac devices.
Proceedings of the IEEE International Conference on Bioinformatics and Biomedicine, 2016
2015
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015
Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 2015
Formal Analysis Provides Parameters for Guiding Hyperoxidation in Bacteria using Phototoxic Proteins.
Proceedings of the 25th edition on Great Lakes Symposium on VLSI, GLVLSI 2015, Pittsburgh, PA, USA, May 20, 2015
SReach: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems.
Proceedings of the Computational Methods in Systems Biology, 2015
2014
SReach: Combining Statistical Tests and Bounded Model Checking for Nonlinear Hybrid Systems with Parametric Uncertainty.
CoRR, 2014
Pathway-gene identification for pancreatic cancer survival via doubly regularized Cox regression.
BMC Syst. Biol., 2014
Proceedings of the 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2014
Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems with Application to Patient-Specific Cardiac Dynamics and Devices.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, 2014
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, 2014
Proceedings of the Perspectives of System Informatics, 2014
Proceedings of the Computational Methods in Systems Biology, 2014
2013
Bayesian statistical model checking with application to Stateflow/Simulink verification.
Formal Methods Syst. Des., 2013
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013
Proceedings of the Testing Software and Systems, 2013
Proceedings of the Formal Methods in Computer-Aided Design, 2013
Proceedings of the Principles and Practice of Constraint Programming, 2013
Proceedings of the Computer Aided Verification - 25th International Conference, 2013
Proceedings of the Automated Deduction - CADE-24, 2013
Studies of biological networks with statistical model checking: application to immune system cells.
Proceedings of the ACM Conference on Bioinformatics, 2013
2012
Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, 2012
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012
Proceedings of the Hybrid Systems: Computation and Control (part of CPS Week 2012), 2012
Proceedings of the Formal Aspects of Component Software, 9th International Symposium, 2012
Proceedings of the Computer Aided Verification - 24th International Conference, 2012
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012
Proceedings of the ACM Turing Centenary Celebration, 2012
2011
Proceedings of the Tools for Practical Software Verification, 2011
Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, 2011
Proceedings of the Algebraic Informatics - 4th International Conference, 2011
Proceedings of the Automated Technology for Verification and Analysis, 2011
Proceedings of the 16th Asia South Pacific Design Automation Conference, 2011
2010
Formal Methods Syst. Des., 2010
Proceedings of the Formal Methods: Foundations and Applications, 2010
Proceedings of the Theory and Applications of Satisfiability Testing, 2010
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010
Bayesian statistical model checking with application to Simulink/Stateflow verification.
Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, 2010
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010
Proceedings of the Time for Verification, 2010
Proceedings of the Algebraic and Numeric Biology - 4th International Conference, 2010
2009
Formal Methods Syst. Des., 2009
Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations.
Formal Methods Syst. Des., 2009
IEEE Des. Test Comput., 2009
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009
Proceedings of the FM 2009: Formal Methods, 2009
Proceedings of the 46th Design Automation Conference, 2009
Proceedings of the Computational Methods in Systems Biology, 7th International Conference, 2009
2008
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2008
Formal Methods Syst. Des., 2008
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008
Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008
Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic.
Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008
Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008
Proceedings of the Logic for Programming, 2008
Proceedings of the Hybrid Systems: Computation and Control, 11th International Workshop, 2008
Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator.
Proceedings of the Hardware and Software: Verification and Testing, 2008
Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway.
Proceedings of the Computational Methods in Systems Biology, 6th International Conference, 2008
Proceedings of the American Control Conference, 2008
2007
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007
Proceedings of the Static Analysis, 14th International Symposium, 2007
Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007
Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007
Proceedings of the Computer Aided Verification, 19th International Conference, 2007
2006
Proceedings of the Verification, 2006
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006
Proceedings of the Theory and Applications of Satisfiability Testing, 2006
Proceedings of the Recent Advances in Intrusion Detection, 9th International Symposium, 2006
2005
Int. J. Softw. Tools Technol. Transf., 2005
Formal Aspects Comput., 2005
Proceedings of the Verified Software: Theories, 2005
Grand Challenge: Model Check Software.
Proceedings of the Verification of Infinite-State Systems with Applications to Security, 2005
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005
Proceedings of the Integrated Formal Methods, 5th International Conference, 2005
Proceedings of the 23rd International Conference on Computer Design (ICCD 2005), 2005
Proceedings of the Hybrid Systems: Computation and Control, 8th International Workshop, 2005
Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005
Proceedings of the FM 2005: Formal Methods, 2005
Proceedings of the 42nd Design Automation Conference, 2005
Proceedings of the Computer Aided Verification, 17th International Conference, 2005
Temporal Logic Model Checking.
Proceedings of the Handbook of Networked and Embedded Control Systems, 2005
2004
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2004
Formal Methods Syst. Des., 2004
Proceedings of the Verification, 2004
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004
Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 2004
Proceedings of the Integrated Formal Methods, 4th International Conference, 2004
Proceedings of the Formal Methods and Software Engineering, 2004
Proceedings of the Formal Methods and Software Engineering, 2004
Proceedings of the 2004 International Conference on Computer-Aided Design, 2004
Proceedings of the 41th Design Automation Conference, 2004
Proceedings of the CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31, 2004
2003
Int. J. Softw. Tools Technol. Transf., 2003
J. ACM, 2003
Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems.
Int. J. Found. Comput. Sci., 2003
Proceedings of the 6th Brazilian Workshop on Formal Methods, 2003
Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach.
Proceedings of the 2003 Workshop on Software Model Checking, 2003
Proceedings of the 10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003), 2003
Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003
Proceedings of the Theory and Applications of Satisfiability Testing, 2003
Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003
Proceedings of the 21st International Conference on Computer Design (ICCD 2003), 2003
Proceedings of the 21st International Conference on Computer Design (ICCD 2003), 2003
Proceedings of the 2003 International Conference on Dependable Systems and Networks (DSN 2003), 2003
Proceedings of the 40th Design Automation Conference, 2003
Proceedings of the Correct Hardware Design and Verification Methods, 2003
Proceedings of the Computer Aided Verification, 15th International Conference, 2003
Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003
Proceedings of the Verification: Theory and Practice, 2003
Proceedings of the 2003 Asia and South Pacific Design Automation Conference, 2003
2002
Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function.
Formal Methods Syst. Des., 2002
Proceedings of the Model Checking of Software, 2002
Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002
Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis.
Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002
Proceedings of the Computer Aided Verification, 14th International Conference, 2002
Proceedings of the Computer Aided Verification, 14th International Conference, 2002
2001
Theor. Comput. Sci., 2001
Proceedings of the 23rd International Conference on Software Engineering, 2001
Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, 2001
Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop 2001, 2001
Proceedings of the Informatics - 10 Years Back. 10 Years Ahead., 2001
Proceedings of the Correct Hardware Design and Verification Methods, 2001
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001
2000
ACM SIGSOFT Softw. Eng. Notes, 2000
Verification of a safety-critical railway interlocking system with real-time constraints.
Sci. Comput. Program., 2000
Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System.
Formal Methods Syst. Des., 2000
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000
Proceedings of the 37th Conference on Design Automation, 2000
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000
Proceedings of the Computer Aided Verification, 12th International Conference, 2000
Model checking algorithms for the µ-calculus.
Proceedings of the Proof, Language, and Interaction, Essays in Honour of Robin Milner, 2000
1999
Int. J. Softw. Tools Technol. Transf., 1999
Analysis and Verification of Real-Time Systems Using Quantitative Symbolic Algorithms.
Int. J. Softw. Tools Technol. Transf., 1999
Formal Methods Syst. Des., 1999
Proceedings of the First International Workshop on Symbolic Model Checking, 1999
Proceedings of the First International Workshop on Symbolic Model Checking, 1999
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1999
Proceedings of the 36th Conference on Design Automation, 1999
Proceedings of the Correct Hardware Design and Verification Methods, 1999
Proceedings of the Correct Hardware Design and Verification Methods, 1999
Proceedings of the Computer Aided Verification, 11th International Conference, 1999
Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999
Multiple State and Single State Tableaux for Combining Local and Global Model Checking.
Proceedings of the Correct System Design, 1999
Proceedings of the Formal Methods for Real-Time and Probabilistic Systems, 1999
1998
J. Autom. Reason., 1998
Proceedings of the First International Workshop on Probabilistic Methods in Verification, 1998
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1998
Proceedings of the 11th Annual Symposium on Integrated Circuits Design, 1998
Using state space exploration and a natural deduction style message derivation engine to verify security protocols.
Proceedings of the Programming Concepts and Methods, 1998
Proceedings of the Formal Methods in Computer-Aided Design, 1998
Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification.
Proceedings of the Formal Methods in Computer-Aided Design, 1998
Proceedings of the Computer Aided Verification, 10th International Conference, 1998
1997
Theor. Comput. Sci., 1997
Sci. Comput. Program., 1997
Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping.
Formal Methods Syst. Des., 1997
Temporal Logic Model Checking (Abstract).
Proceedings of the Logic Programming, 1997
Proceedings of the Proceedings 1997 International Conference on Computer Design: VLSI in Computers & Processors, 1997
Proceedings of the Automata, Languages and Programming, 24th International Colloquium, 1997
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1997
Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997
The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997
1996
Formal Methods Syst. Des., 1996
Model checking.
Proceedings of the NATO Advanced Study Institute on Deductive Program Design, 1996
Proceedings of the Mathematical Foundations of Computer Science 1996, 1996
Proceedings of the 1996 IEEE International Conference on Robotics and Automation, 1996
Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking.
Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996
Proceedings of the 33st Conference on Design Automation, 1996
Proceedings of the Computer Aided Verification, 8th International Conference, 1996
1995
Formal Methods Syst. Des., 1995
Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques, 1995
Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques, 1995
Proceedings of the ACM SIGPLAN 1995 Workshop on Languages, 1995
Proceedings of the 1995 International Conference on Computer Design (ICCD '95), 1995
Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, 1995
Proceedings of the 32st Conference on Design Automation, 1995
Proceedings of the CONCUR '95: Concurrency Theory, 1995
Proceedings of the Computer Science Today: Recent Trends and Developments, 1995
1994
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994
Proceedings of the 15th IEEE Real-Time Systems Symposium (RTSS '94), 1994
Proceedings of the 1994 IEEE International Symposium on Circuits and Systems, ISCAS 1994, London, England, UK, May 30, 1994
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994
Proceedings of the Application and Theory of Petri Nets 1994, 1994
1993
A Unified Approch for Showing Language Inclusion and Equivalence Between Various Types of omega-Automata.
Inf. Process. Lett., 1993
Proceedings of the A Decade of Concurrency, Reflections and Perspectives, 1993
Automatic Verification of Sequential Circuit Designs.
Proceedings of the Computer Hardware Description Languages and their Applications, Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications, 1993
Proceedings of the Computer Aided Verification, 5th International Conference, 1993
Proceedings of the Computer Aided Verification, 5th International Conference, 1993
1992
J. Log. Comput., 1992
Proceedings of the Automated Deduction, 1992
1991
A language for compositional specification and verification of finite state hardware controllers.
Proc. IEEE, 1991
Symbolic Model Checking with Partitioned Transistion Relations.
Proceedings of the VLSI 91, 1991
Proceedings of the 28th Design Automation Conference, 1991
1990
Proceedings of the 1990 IEEE International Conference on Computer Design: VLSI in Computers and Processors, 1990
Preface.
Proceedings of the Computer-Aided Verification, 1990
Proceedings of the 27th ACM/IEEE Design Automation Conference. Orlando, 1990
Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem.
Proceedings of the Computer Aided Verification, 2nd International Workshop, 1990
A Unified Approach For Showing Language Containment And Equivalence Between Various Types Of Omega-Automata.
Proceedings of the CAAP '90, 1990
1989
Inf. Comput., December, 1989
Inf. Comput., April, 1989
Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989
1988
Theor. Comput. Sci., 1988
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1988
Proceedings of the Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands, May 30, 1988
Proceedings of the 9th International Conference on Automated Deduction, 1988
1987
Proceedings of the Temporal Logic in Specification, 1987
Proceedings of the TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1987
Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, 1987
1986
Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications.
ACM Trans. Program. Lang. Syst., 1986
IEEE Trans. Computers, 1986
True Relative Completeness of an Axiom System for the Language L4 (Abridged)
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986
1985
Theor. Comput. Sci., 1985
1984
Proceedings of the Logics and Models of Concurrent Systems, 1984
1983
Proceedings of the symposium on Communications Architectures & Protocols, 1983
Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach.
Proceedings of the Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, 1983
Proceedings of the Logics of Programs, 1983
Proceedings of the Logics of Programs, 1983
1982
IEEE Trans. Computers, 1982
Sci. Comput. Program., 1982
Proceedings of the ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, 1982
1981
Softw. Pract. Exp., 1981
1980
ACM Trans. Program. Lang. Syst., 1980
Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data.
Proceedings of the Sixth International Conference on Very Large Data Bases, 1980
Proceedings of the Automata, 1980
1979
Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems.
J. ACM, 1979
Approximate Algorithms for Optimization of Busy Waiting in Parallel Programs (Preliminary Report)
Proceedings of the 20th Annual Symposium on Foundations of Computer Science, 1979
1977
Programming Language Constructs for Which it is Impossible to Obtain "Good" Hoare-Like Axiom Systems.
Proceedings of the Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, 1977
Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October, 1977
1976
Completeness and Incompleteness Theorems for Hoare-like Axiom Systems.
PhD thesis, 1976