| 2015 | CAV | From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis. | Pavol Cern, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach |
| 2015 | TACAS | dReach: δ-Reachability Analysis for Hybrid Systems. | Soonho Kong, Sicun Gao, Wei Chen, Edmund M. Clarke |
| 2014 | ISoLA | Model Checking Hybrid Systems - (Invited Talk). | Edmund M. Clarke, Sicun Gao |
| 2014 | ISoLA | Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems with Application to Patient-Specific Cardiac Dynamics and Devices. | Radu Grosu, Elizabeth Cherry, Edmund M. Clarke, Rance Cleaveland, Sanjay Dixit, Flavio H. Fenton, Sicun Gao, James Glimm, Richard A. Gray, Rahul Mangharam, Arnab Ray, Scott A. Smolka |
| 2014 | SYNASC | Proof Generation from Delta-Decisions. | Sicun Gao, Soonho Kong, Edmund M. Clarke |
| 2013 | CADE | dReal: An SMT Solver for Nonlinear Theories over the Reals. | Sicun Gao, Soonho Kong, Edmund M. Clarke |
| 2013 | CAV | Automatic Abstraction in SMT-Based Unbounded Software Model Checking. | Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, Edmund M. Clarke |
| 2013 | CP | Solving QBF with Free Variables. | William Klieber, Mikols Janota, Joo Marques-Silva, Edmund M. Clarke |
| 2013 | FMCAD | Satisfiability modulo ODEs. | Sicun Gao, Soonho Kong, Edmund M. Clarke |
| 2013 | SAT | Turing's Computable Real Numbers and Why They Are Still Important Today. | Edmund M. Clarke |
| 2012 | CADE | δ-Complete Decision Procedures for Satisfiability over the Reals. | Sicun Gao, Jeremy Avigad, Edmund M. Clarke |
| 2012 | CAV | Assume-Guarantee Abstraction Refinement for Probabilistic Systems. | Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke |
| 2012 | LICS | Delta-Decidability over the Reals. | Sicun Gao, Jeremy Avigad, Edmund M. Clarke |
| 2012 | LICS | Learning Probabilistic Systems from Tree Samples. | Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke |
| 2012 | SAT | Solving QBF with Counterexample Guided Refinement. | Mikols Janota, William Klieber, Joo Marques-Silva, Edmund M. Clarke |
| 2011 | ASPDAC | Analog circuit verification by statistical model checking. | Ying-Chih Wang, Anvesh Komuravelli, Paolo Zuliani, Edmund M. Clarke |
| 2011 | ATVA | Statistical Model Checking for Cyber-Physical Systems. | Edmund M. Clarke, Paolo Zuliani |
| 2010 | CAV | Automated Assume-Guarantee Reasoning through Implicit Learning. | Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang |
| 2010 | FMCAD | Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. | Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke |
| 2010 | ISoLA | Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. | Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, Lei Zhu |
| 2010 | SAT | A Non-prenex, Non-clausal QBF Solver with Game-State Learning. | William Klieber, Samir Sapra, Sicun Gao, Edmund M. Clarke |
| 2009 | DAC | Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts. | Himanshu Jain, Edmund M. Clarke |
| 2009 | FM | Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. | Andr Platzer, Edmund M. Clarke |
| 2009 | LICS | My 27-year Quest to Overcome the State Explosion Problem. | Edmund M. Clarke |
| 2009 | TACAS | Learning Minimal Separating DFA's for Compositional Verification. | Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang |
| 2008 | CAV | Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. | Himanshu Jain, Edmund M. Clarke, Orna Grumberg |
| 2008 | CAV | Computing Differential Invariants of Hybrid Systems as Fixedpoints. | Andr Platzer, Edmund M. Clarke |
| 2008 | LPAR | Model Checking - My 27-Year Quest to Overcome the State Explosion Problem. | Edmund M. Clarke |
| 2008 | TACAS | Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. | Edmund M. Clarke, Muralidhar Talupur, Helmut Veith |
| 2008 | TACAS | Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. | Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang |
| 2007 | CAV | SAT-Based Compositional Verification Using Lazy Learning. | Nishant Sinha, Edmund M. Clarke |
| 2007 | SAS | Arithmetic Strengthening for Shape Analysis. | Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook |
| 2007 | TACAS | VCEGAR: Verilog CounterExample Guided Abstraction Refinement. | Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke |
| 2006 | RAID | Ranking Attack Graphs. | Vaibhav Mehta, Constantinos Bartzis, Haifeng Zhu, Edmund M. Clarke, Jeannette M. Wing |
| 2006 | SAT | Satisfiability Checking of Non-clausal Formulas Using General Matings. | Himanshu Jain, Constantinos Bartzis, Edmund M. Clarke |
| 2006 | TACAS | Verifying Concurrent Message-Passing C Programs with Recursive Calls. | Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili |
| 2006 | VMCAI | Environment Abstraction for Parameterized Verification. | Edmund M. Clarke, Muralidhar Talupur, Helmut Veith |
| 2005 | CAV | Automated Assume-Guarantee Reasoning for Simulation Conformance. | Sagar Chaki, Edmund M. Clarke, Nishant Sinha, Prasanna Thati |
| 2005 | DAC | Word level predicate abstraction and refinement for verifying RTL verilog. | Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke |
| 2005 | FM | Dynamic Component Substitutability Analysis. | Natasha Sharygina, Sagar Chaki, Edmund M. Clarke, Nishant Sinha |
| 2005 | ICCD | Reconsidering CEGAR: Learning Good Abstractions without Refinement. | Anubhav Gupta, Edmund M. Clarke |
| 2005 | IFM | State/Event Software Verification for Branching-Time Specifications. | Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Jol Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith |
| 2005 | TACAS | SATABS: SAT-Based Predicate Abstraction for ANSI-C. | Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav |
| 2004 | CONCUR | Verification by Network Decomposition. | Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, Helmut Veith |
| 2004 | DAC | A SAT-based algorithm for reparameterization in symbolic simulation. | Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening |
| 2004 | ICCAD | Checking consistency of C and Verilog using predicate abstraction and induction. | Daniel Kroening, Edmund M. Clarke |
| 2004 | ICFEM | Tutorial: Software Model Checking. | Edmund M. Clarke, Daniel Kroening |
| 2004 | ICFEM | Counterexample Guided Abstraction Refinement Via Program Execution. | Daniel Kroening, Alex Groce, Edmund M. Clarke |
| 2004 | IFM | State/Event-Based Software Model Checking. | Sagar Chaki, Edmund M. Clarke, Jol Ouaknine, Natasha Sharygina, Nishant Sinha |
| 2004 | MEMOCODE | Automated, compositional and iterative deadlock detection. | Sagar Chaki, Edmund M. Clarke, Jol Ouaknine, Natasha Sharygina |
| 2004 | MEMOCODE | Verification of SpecC using predicate abstraction. | Himanshu Jain, Daniel Kroening, Edmund M. Clarke |
| 2004 | TACAS | A Tool for Checking ANSI-C Programs. | Edmund M. Clarke, Daniel Kroening, Flavio Lerda |
| 2004 | VMCAI | Completeness and Complexity of Bounded Model Checking. | Edmund M. Clarke, Daniel Kroening, Jol Ouaknine, Ofer Strichman |
| 2003 | ASPDAC | Hardware verification using ANSI-C programs as a reference. | Edmund M. Clarke, Daniel Kroening |
| 2003 | CADE | SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. | Edmund M. Clarke |
| 2003 | CAV | Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. | Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang |
| 2003 | DAC | Behavioral consistency of C and verilog programs using bounded model checking. | Edmund M. Clarke, Daniel Kroening, Karen Yorav |
| 2003 | DSN | Model Checking for Dependable Software-Intensive Systems. | Edmund M. Clarke, Masahiro Fujita, David P. Gluch |
| 2003 | ICCD | Specifying and Verifying Systems with Multiple Clocks. | Edmund M. Clarke, Daniel Kroening, Karen Yorav |
| 2003 | ICCD | SAT-Based Algorithms for Logic Minimization. | Samir Sapra, Michael Theobald, Edmund M. Clarke |
| 2003 | ICSE | Modular Verification of Software Components in C. | Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith |
| 2003 | MEMOCODE | High Level Verification of Control Intensive Systems Using Predicate Abstraction. | Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang |
| 2003 | SAT | SAT Based Predicate Abstraction for Hardware Verification. | Edmund M. Clarke, Muralidhar Talupur, Helmut Veith, Dong Wang |
| 2003 | TACAS | Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. | Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Olaf Stursberg, Michael Theobald |
| 2003 | TIME | Counterexample-Guided Abstraction Refinement. | Edmund M. Clarke |
| 2002 | CAV | 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 |
| 2002 | CAV | SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. | Edmund M. Clarke, Anubhav Gupta, James H. Kukula, Ofer Strichman |
| 2002 | FMCAD | Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis. | Pankaj Chauhan, Edmund M. Clarke, James H. Kukula, Samir Sapra, Helmut Veith, Dong Wang |
| 2002 | LICS | Tree-Like Counterexamples in Model Checking. | Edmund M. Clarke, Somesh Jha, Yuan Lu, Helmut Veith |
| 2001 | ICCAD | Non-linear Quantification Scheduling in Image Computation. | Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Thomas R. Shiple, Helmut Veith, Dong Wang |
| 2001 | ICSE | Efficient Filtering in Publish-Subscribe Systems Using Binary Decision. | Alexis Campailla, Sagar Chaki, Edmund M. Clarke, Somesh Jha, Helmut Veith |
| 2000 | CAV | Counterexample-Guided Abstraction Refinement. | Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith |
| 2000 | CAV | Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. | Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta |
| 2000 | DAC | Efficient variable ordering using aBDD based sampling. | Yuan Lu, Jawahar Jain, Edmund M. Clarke, Masahiro Fujita |
| 2000 | FMCAD | A Theory of Consistency for Modular Synchronous Systems. | Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel |
| 2000 | FMCAD | Executable Protocol Specification in ESL. | Edmund M. Clarke, Steven M. German, Yuan Lu, Helmut Veith, Dong Wang |
| 2000 | TACAS | Partial Order Reductions for Security Protocol Verification. | Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero |
| 1999 | CAV | Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. | Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu |
| 1999 | CAV | NUSMV: A New Symbolic Model Verifier. | Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri |
| 1999 | DAC | Symbolic Model Checking Using SAT Procedures instead of BDDs. | Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, Yunshan Zhu |
| 1999 | TACAS | Symbolic Model Checking without BDDs. | Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu |
| 1998 | CAV | Symmetry Reductions in Model Checking. | Edmund M. Clarke, E. Allen Emerson, Somesh Jha, A. Prasad Sistla |
| 1998 | FMCAD | Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. | Sergey Berezin, Armin Biere, Edmund M. Clarke, Yunshan Zhu |
| 1998 | FMCAD | Model Checking VHDL with CV. | David Dharbe, Subash Shankar, Edmund M. Clarke |
| 1998 | TABLEAUX | Model Checking: Historical Perspective and Example (Extended Abstract). | Edmund M. Clarke, Sergey Berezin |
| 1997 | CAV | The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems. | Srgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea |
| 1997 | ICALP | Symbolic Model Checking for Probabilistic Processes. | Christel Baier, Edmund M. Clarke, Vasiliki Hartonas-Garmhausen, Marta Z. Kwiatkowska, Mark Ryan |
| 1997 | ICCD | Equivalence Checking Using Abstract BDDs. | Somesh Jha, Yuan Lu, Marius Minea, Edmund M. Clarke |
| 1996 | AISC | Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation. | Andrej Bauer, Edmund M. Clarke, Xudong Zhao |
| 1996 | CAV | Verifying the SRT Division Algorithm Using Theorem Proving Techniques. | Edmund M. Clarke, Steven M. German, Xudong Zhao |
| 1996 | CAV | Symbolic Model Checking. | Edmund M. Clarke, Kenneth L. McMillan, Srgio Vale Aguiar Campos, Vasiliki Hartonas-Garmhausen |
| 1996 | DAC | Word Level Model Checking - Avoiding the Pentium FDIV Error. | Edmund M. Clarke, Manpreet Khaira, Xudong Zhao |
| 1996 | FMCAD | Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking. | Yirng-An Chen, Edmund M. Clarke, Pei-Hsin Ho, Yatin Vasant Hoskote, Timothy Kam, Manpreet Khaira, John W. O'Leary, Xudong Zhao |
| 1996 | ICRA | Deadlock prevention in flexible manufacturing systems using symbolic model checking. | Vasiliki Hartonas-Garmhausen, Edmund M. Clarke, S. Campos |
| 1996 | MFCS | Word Level Model Checking (Abstract). | Edmund M. Clarke, Xudong Zhao |
| 1995 | CONCUR | Veryfying Parameterized Networks using Abstraction and Regular Languages. | Edmund M. Clarke, Orna Grumberg, Somesh Jha |
| 1995 | DAC | Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. | Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao |
| 1995 | ICCAD | Hybrid decision diagrams. | Edmund M. Clarke, Masahiro Fujita, Xudong Zhao |
| 1995 | ICCD | Verifying the performance of the PCI local bus using symbolic techniques. | Srgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea |
| 1994 | CADE | Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan. | Edmund M. Clarke, Xudong Zhao |
| 1994 | CAV | Another Look at LTL Model Checking. | Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi |
| 1994 | CAV | An Improved Algorithm for the Evaluation of Fixpoint Expressions. | David E. Long, Anca Browne, Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero |
| 1994 | ISCAS | Fast Spectrum Computation for Logic Functions using Binary Decision Diagrams. | Masahiro Fujita, Jerry Chih-Yuan Yang, Edmund M. Clarke, Xudong Zhao, Patrick C. McGeer |
| 1994 | LICS | Automatic Verification of Finite-State Concurrent Systems | Edmund M. Clarke |
| 1994 | RTSS | Computing Quantitative Characteristics of Finite-State Real-Time Systems. | Srgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea, Hiromi Hiraishi |
| 1993 | CAV | Exploiting Symmetry In Temporal Logic Model Checking. | Edmund M. Clarke, Thomas Filkorn, Somesh Jha |
| 1993 | CAV | Efficient Verification of Parallel Real-Time Systems. | Tomohiro Yoneda, Atsufumi Shibayama, Bernd-Holger Schlingloff, Edmund M. Clarke |
| 1993 | DAC | Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. | Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, Jerry Chih-Yuan Yang |
| 1992 | CADE | Analytica - A Theorem Prover in Mathematica. | Edmund M. Clarke, Xudong Zhao |
| 1992 | POPL | Model Checking and Abstraction. | Edmund M. Clarke, Orna Grumberg, David E. Long |
| 1991 | DAC | Representing Circuits More Efficiently in Symbolic Model Checking. | Jerry R. Burch, Edmund M. Clarke, David E. Long |
| 1990 | CAV | Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem. | Edmund M. Clarke |
| 1990 | DAC | Sequential Circuit Verification Using Symbolic Model Checking. | Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill |
| 1990 | ICCD | A parallel algorithm for constructing binary decision diagrams. | Shinji Kimura, Edmund M. Clarke |
| 1990 | LICS | Symbolic Model Checking: 10^20 States and Beyond | Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang |
| 1989 | LICS | PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses | Soumitra Bose, Edmund M. Clarke, David E. Long, Spiro Michaylov |
| 1989 | LICS | Compositional Model Checking | Edmund M. Clarke, David E. Long, Kenneth L. McMillan |
| 1988 | CADE | PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. | P. E. Allen, Soumitra Bose, Edmund M. Clarke, Spiro Michaylov |
| 1987 | PODC | Avoiding The State Explosion Problem in Temporal Logic Model Checking. | Edmund M. Clarke, Orna Grumberg |
| 1986 | DAC | Escher - a geometrical layout system for recursively defined circuits. | Edmund M. Clarke, Yulin Feng |
| 1986 | LICS | True Relative Completeness of an Axiom System for the Language L4 (Abridged) | Steven M. German, Edmund M. Clarke, Joseph Y. Halpern |
| 1986 | PODC | Reasoning About Networks With Many Identical Finite-State Processes. | Edmund M. Clarke, Orna Grumberg, Michael C. Browne |
| 1985 | POPL | Compiling Path Expressions into VLSI Circuits. | Thomas S. Anantharaman, Edmund M. Clarke, Michael J. Foster, Bud Mishra |
| 1983 | POPL | Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. | Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla |
| 1983 | SIGCOMM | A methodology for verifying request processing protocols. | Christos Nikolaou, Edmund M. Clarke, Nissim Francez, Stephen A. Schuman |
| 1982 | PODC | Can Message Buffers be Characterized in Linear Temporal Logic? | A. Prasad Sistla, Edmund M. Clarke, Nissim Francez, Yuri Gurevich |
| 1982 | POPL | On Effective Axiomatizations of Hoare Logics. | Edmund M. Clarke, Steven M. German, Joseph Y. Halpern |
| 1982 | STOC | The Complexity of Propositional Linear Temporal Logics | A. Prasad Sistla, Edmund M. Clarke |
| 1980 | ICALP | Characterizing Correctness Properties of Parallel Programs Using Fixpoints. | E. Allen Emerson, Edmund M. Clarke |
| 1980 | VLDB | Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data. | Philip A. Bernstein, Barbara T. Blaustein, Edmund M. Clarke |
| 1979 | FOCS | Approximate Algorithms for Optimization of Busy Waiting in Parallel Programs (Preliminary Report) | Edmund M. Clarke, Lishing Liu |
| 1979 | POPL | Synthesis of Resource Invariants for Concurrent Programs. | Edmund M. Clarke |
| 1977 | FOCS | Program Invariants as Fixed Points (Preliminary Reports) | Edmund M. Clarke |
| 1977 | POPL | Programming Language Constructs for Which it is Impossible to Obtain "Good" Hoare-Like Axiom Systems. | Edmund M. Clarke |