Edmund M. Clarke

Sicun Gao, Jeremy Avigad, Edmund M. Clarke: δ-Complete Decision Procedures for Satisfiability over the Reals. IJCAR 2012: 286-300

Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke: Assume-Guarantee Abstraction Refinement for Probabilistic Systems. CAV 2012: 310-326

Qiusong Yang, Edmund M. Clarke, Anvesh Komuravelli, Mingshu Li: Assumption Generation for Asynchronous Systems by Abstraction Refinement. FACS 2012: 260-276

Paolo Zuliani, Christel Baier, Edmund M. Clarke: Rare-event verification for stochastic hybrid systems. HSCC 2012: 217-226

Sicun Gao, Jeremy Avigad, Edmund M. Clarke: Delta-Decidability over the Reals. LICS 2012: 305-314

Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke: Learning Probabilistic Systems from Tree Samples. LICS 2012: 441-450

David Henriques, João Martins, Paolo Zuliani, André Platzer, Edmund M. Clarke: Statistical Model Checking for Markov Decision Processes. QEST 2012: 84-93

Mikolás Janota, William Klieber, João Marques-Silva, Edmund M. Clarke: Solving QBF with Counterexample Guided Refinement. SAT 2012: 114-128

Edmund M. Clarke, Irina Virbitskaite, Andrei Voronkov (Eds.): Perspectives of Systems Informatics - 8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27-July 1, 2011, Revised Selected Papers. Lecture Notes in Computer Science 7162, Springer 2012, isbn 978-3-642-29708-3

Sicun Gao, Jeremy Avigad, Edmund M. Clarke: Delta-Complete Decision Procedures for Satisfiability over the Reals. CoRR abs/1204.3513 (2012)

Sicun Gao, Jeremy Avigad, Edmund M. Clarke: Delta-Decidability over the Reals. CoRR abs/1204.6671 (2012)

Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke: Assume-Guarantee Abstraction Refinement for Probabilistic Systems. CoRR abs/1207.5086 (2012)

Anvesh Komuravelli, Corina S. Pasareanu, Edmund M. Clarke: Learning Probabilistic Systems from Tree Samples. CoRR abs/1207.5091 (2012)

Ying-Chih Wang, Anvesh Komuravelli, Paolo Zuliani, Edmund M. Clarke: Analog circuit verification by statistical model checking. ASP-DAC 2011: 1-6

Edmund M. Clarke, Paolo Zuliani: Statistical Model Checking for Cyber-Physical Systems. ATVA 2011: 1-12

Sicun Gao, André Platzer, Edmund M. Clarke: Quantifier Elimination over Finite Fields Using Gröbner Bases. CAI 2011: 140-157

Haijun Gong, Paolo Zuliani, Qinsi Wang, Edmund M. Clarke: Formal analysis for logical models of pancreatic cancer. CDC-ECE 2011: 4855-4860

Sicun Gao, André Platzer, Edmund M. Clarke: Quantifier Elimination over Finite Fields Using Gröbner Bases. CoRR abs/1104.0746 (2011)

Haijun Gong, Paolo Zuliani, Anvesh Komuravelli, James R. Faeder, Edmund M. Clarke: Analysis and verification of the HMGB1 signaling pathway. BMC Bioinformatics 11(S-7): S10 (2010)

Edmund M. Clarke, Alexandre Donzé, Axel Legay: On simulation-based probabilistic model checking of mixed-analog circuits. Formal Methods in System Design 36(2): 97-113 (2010)

Haijun Gong, Paolo Zuliani, Anvesh Komuravelli, James R. Faeder, Edmund M. Clarke: Computational Modeling and Verification of Signaling Pathways in Cancer. ANB 2010: 117-135

Edmund M. Clarke, Robert P. Kurshan, Helmut Veith: The Localization Reduction and Counterexample-Guided Abstraction Refinement. Essays in Memory of Amir Pnueli 2010: 61-71

Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang: Automated Assume-Guarantee Reasoning through Implicit Learning. CAV 2010: 511-526

Sicun Gao, Malay K. Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, Edmund M. Clarke: Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. FMCAD 2010: 81-89

Paolo Zuliani, André Platzer, Edmund M. Clarke: Bayesian statistical model checking with application to Simulink/Stateflow verification. HSCC 2010: 243-252

Yu-Fang Chen, Edmund M. Clarke, Azadeh Farzan, Fei He, Ming-Hsien Tsai, Yih-Kuen Tsay, Bow-Yaw Wang, Lei Zhu: Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. ISoLA (1) 2010: 643-657

William Klieber, Samir Sapra, Sicun Gao, Edmund M. Clarke: A Non-prenex, Non-clausal QBF Solver with Game-State Learning. SAT 2010: 128-142

Håkan L. S. Younes, Edmund M. Clarke, Paolo Zuliani: Statistical Verification of Probabilistic Properties with Unbounded Until. SBMF 2010: 144-160

Edmund M. Clarke, Andrei Voronkov (Eds.): Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers. Lecture Notes in Computer Science 6355, Springer 2010, isbn 978-3-642-17510-7

Edmund M. Clarke, E. Allen Emerson, Joseph Sifakis: Model checking: algorithmic verification and debugging. Commun. ACM 52(11): 74-84 (2009)

Anmol Mathur, Masahiro Fujita, Edmund M. Clarke, Pascal Urard: Functional Equivalence Verification Tools in High-Level Synthesis Flows. IEEE Design & Test of Computers 26(4): 88-95 (2009)

Himanshu Jain, Edmund M. Clarke, Orna Grumberg: Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations. Formal Methods in System Design 35(1): 6-39 (2009)

André Platzer, Edmund M. Clarke: Computing differential invariants of hybrid systems as fixedpoints. Formal Methods in System Design 35(1): 98-120 (2009)

Sumit Kumar Jha, Edmund M. Clarke, Christopher James Langmead, Axel Legay, André Platzer, Paolo Zuliani: A Bayesian Approach to Model Checking Biological Systems. CMSB 2009: 218-234

Himanshu Jain, Edmund M. Clarke: Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts. DAC 2009: 563-568

André Platzer, Edmund M. Clarke: Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. FM 2009: 547-562

Edmund M. Clarke: My 27-year Quest to Overcome the State Explosion Problem. LICS 2009: 3

Edmund M. Clarke: Model Checking - My 27-year Quest to Overcome the State Explosion Problem. NASA Formal Methods 2009: 1

Yu-Fang Chen, Azadeh Farzan, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang: Learning Minimal Separating DFA's for Compositional Verification. TACAS 2009: 31-45

Sagar Chaki, Edmund M. Clarke, Natasha Sharygina, Nishant Sinha: Verification of evolving software via component substitutability analysis. Formal Methods in System Design 32(3): 235-266 (2008)

Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke: Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog. IEEE Trans. on CAD of Integrated Circuits and Systems 27(2): 366-379 (2008)

André Platzer, Edmund M. Clarke: Computing Differential Invariants of Hybrid Systems as Fixedpoints. CAV 2008: 176-189

Himanshu Jain, Edmund M. Clarke, Orna Grumberg: Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. CAV 2008: 254-267

Edmund M. Clarke, James R. Faeder, Christopher James Langmead, Leonard A. Harris, Sumit Kumar Jha, Axel Legay: Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway. CMSB 2008: 231-250

Edmund M. Clarke, Alexandre Donzé, Axel Legay: Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator. Haifa Verification Conference 2008: 149-163

Flavio Lerda, James Kapinski, Edmund M. Clarke, Bruce H. Krogh: Verification of Supervisory Control Software Using State Proximity and Merging. HSCC 2008: 344-357

Edmund M. Clarke: Model Checking - My 27-Year Quest to Overcome the State Explosion Problem. LPAR 2008: 182

Edmund M. Clarke: The Birth of Model Checking. 25 Years of Model Checking 2008: 1-26

Edmund M. Clarke, E. Allen Emerson: Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. 25 Years of Model Checking 2008: 196-215

Azadeh Farzan, Yu-Fang Chen, Edmund M. Clarke, Yih-Kuen Tsay, Bow-Yaw Wang: Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. TACAS 2008: 2-17

Edmund M. Clarke, Muralidhar Talupur, Helmut Veith: Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. TACAS 2008: 33-47

Edmund M. Clarke, Himanshu Jain, Daniel Kroening: Verification of SpecC using predicate abstraction. Formal Methods in System Design 30(1): 5-28 (2007)

Edmund M. Clarke, Flavio Lerda: Model Checking: Software and Beyond. J. UCS 13(5): 639-649 (2007)

Nishant Sinha, Edmund M. Clarke: SAT-Based Compositional Verification Using Lazy Learning. CAV 2007: 39-54

Sumit Kumar Jha, Bruce H. Krogh, James E. Weimer, Edmund M. Clarke: Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction. HSCC 2007: 287-300

André Platzer, Edmund M. Clarke: The Image Computation Problem in Hybrid Systems Model Checking. HSCC 2007: 473-486

Stephen Magill, Josh Berdine, Edmund M. Clarke, Byron Cook: Arithmetic Strengthening for Shape Analysis. SAS 2007: 419-436

Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke: VCEGAR: Verilog CounterExample Guided Abstraction Refinement. TACAS 2007: 583-586

Vaibhav Mehta, Constantinos Bartzis, Haifeng Zhu, Edmund M. Clarke, Jeannette M. Wing: Ranking Attack Graphs. RAID 2006: 127-144

Himanshu Jain, Constantinos Bartzis, Edmund M. Clarke: Satisfiability Checking of Non-clausal Formulas Using General Matings. SAT 2006: 75-89

Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili: Verifying Concurrent Message-Passing C Programs with Recursive Calls. TACAS 2006: 334-349

Edmund M. Clarke, Muralidhar Talupur, Helmut Veith: Environment Abstraction for Parameterized Verification. VMCAI 2006: 126-141

Edmund M. Clarke, Marius Minea, Ferucio Laurentiu Tiplea (Eds.): Verification of Infinite-State Systems with Applications to Security, Proceedings of the NATO Advanced Research Workshop "Verification of Infinite State Systems with Applications to Security VISSAS 2005", Timisoara, Romania, March 17-22, 2005. NATO Security through Science Series D: Information and Communication Security 1, IOS Press 2006, isbn 1-58603-570-3

Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha: Concurrent software verification with states, events, and deadlocks. Formal Asp. Comput. 17(4): 461-483 (2005)

Sagar Chaki, Edmund M. Clarke, Somesh Jha, Helmut Veith: An Iterative Framework for Simulation Conformance. J. Log. Comput. 15(4): 465-488 (2005)

Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman: Computational challenges in bounded model checking. STTT 7(2): 174-183 (2005)

Sagar Chaki, Edmund M. Clarke, Nishant Sinha, Prasanna Thati: Automated Assume-Guarantee Reasoning for Simulation Conformance. CAV 2005: 534-547

Himanshu Jain, Daniel Kroening, Natasha Sharygina, Edmund M. Clarke: Word level predicate abstraction and refinement for verifying RTL verilog. DAC 2005: 445-450

Natasha Sharygina, Sagar Chaki, Edmund M. Clarke, Nishant Sinha: Dynamic Component Substitutability Analysis. FM 2005: 512-528

Edmund M. Clarke, Natasha Sharygina, Nishant Sinha: Program Compatibility Approaches. FMCO 2005: 243-258

Ansgar Fehnker, Edmund M. Clarke, Sumit Kumar Jha, Bruce H. Krogh: Refining Abstractions of Hybrid Systems Using Counterexample Fragments. HSCC 2005: 242-257

Anubhav Gupta, Edmund M. Clarke: Reconsidering CEGAR: Learning Good Abstractions without Refinement. ICCD 2005: 591-598

Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili, Helmut Veith: State/Event Software Verification for Branching-Time Specifications. IFM 2005: 53-69

Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav: SATABS: SAT-Based Predicate Abstraction for ANSI-C. TACAS 2005: 570-574

Edmund M. Clarke, Himanshu Jain, Nishant Sinha: Grand Challenge: Model Check Software. VISSAS 2005: 55-68

Edmund M. Clarke, Anubhav Gupta, Himanshu Jain, Helmut Veith: Model Checking: Back and Forth between Hardware and Software. VSTTE 2005: 251-255

Edmund M. Clarke, Ansgar Fehnker, Sumit Kumar Jha, Helmut Veith: Temporal Logic Model Checking. Handbook of Networked and Embedded Control Systems 2005: 539-558

Edjard Mota, Edmund M. Clarke, Alex Groce, Waleska Oliveira, Marcia Falcão, Jorge Kanda: VeriAgent: an Approach to Integrating UML and Formal Verification Tools. Electr. Notes Theor. Comput. Sci. 95: 111-129 (2004)

Edmund M. Clarke, Daniel Kroening, Natasha Sharygina, Karen Yorav: Predicate Abstraction of ANSI-C Programs Using SAT. Formal Methods in System Design 25(2-3): 105-127 (2004)

Sagar Chaki, Edmund M. Clarke, Alex Groce, Joël Ouaknine, Ofer Strichman, Karen Yorav: Efficient Verification of Sequential and Concurrent C Programs. Formal Methods in System Design 25(2-3): 129-166 (2004)

Edmund M. Clarke, Anubhav Gupta, Ofer Strichman: SAT-based counterexample-guided abstraction refinement. IEEE Trans. on CAD of Integrated Circuits and Systems 23(7): 1113-1123 (2004)

Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith: Modular Verification of Software Components in C. IEEE Trans. Software Eng. 30(6): 388-402 (2004)

Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, Helmut Veith: Verification by Network Decomposition. CONCUR 2004: 276-291

Pankaj Chauhan, Edmund M. Clarke, Daniel Kroening: A SAT-based algorithm for reparameterization in symbolic simulation. DAC 2004: 524-529

Daniel Kroening, Edmund M. Clarke: Checking consistency of C and Verilog using predicate abstraction and induction. ICCAD 2004: 66-72

Edmund M. Clarke, Daniel Kroening: Tutorial: Software Model Checking. ICFEM 2004: 9-10

Daniel Kroening, Alex Groce, Edmund M. Clarke: Counterexample Guided Abstraction Refinement Via Program Execution. ICFEM 2004: 224-238

Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha: State/Event-Based Software Model Checking. IFM 2004: 128-147

Himanshu Jain, Daniel Kroening, Edmund M. Clarke: Verification of SpecC using predicate abstraction. MEMOCODE 2004: 7-16

Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina: Automated, compositional and iterative deadlock detection. MEMOCODE 2004: 201-210

Edmund M. Clarke, Daniel Kroening, Flavio Lerda: A Tool for Checking ANSI-C Programs. TACAS 2004: 168-176

Edmund M. Clarke, Daniel Kroening, Joël Ouaknine, Ofer Strichman: Completeness and Complexity of Bounded Model Checking. VMCAI 2004: 85-96

Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Ofer Strichman, Yunshan Zhu: Bounded model checking. Advances in Computers 58: 117-148 (2003)

Sagar Chaki, Joël Ouaknine, Karen Yorav, Edmund M. Clarke: Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach. Electr. Notes Theor. Comput. Sci. 89(3): 417-432 (2003)

Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Joël Ouaknine, Olaf Stursberg, Michael Theobald: Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. Int. J. Found. Comput. Sci. 14(4): 583-604 (2003)

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5): 752-794 (2003)

Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero: Efficient verification of security protocols using partial-order reductions. STTT 4(2): 173-188 (2003)

Edmund M. Clarke, Daniel Kroening: Hardware verification using ANSI-C programs as a reference. ASP-DAC 2003: 308-311

Edmund M. Clarke, Helmut Veith: Counterexamples Revisited: Principles, Algorithms, Applications. Verification: Theory and Practice 2003: 208-224

Edmund M. Clarke: SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. CADE 2003: 1

Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang: Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. CAV 2003: 126-140

Sagar Chaki, Edmund M. Clarke, Alex Groce, Ofer Strichman: Predicate Abstraction with Minimum Predicates. CHARME 2003: 19-34

Edmund M. Clarke, Daniel Kroening, Karen Yorav: Behavioral consistency of C and verilog programs using bounded model checking. DAC 2003: 368-371

Edmund M. Clarke, Masahiro Fujita, David P. Gluch: Model Checking for Dependable Software-Intensive Systems. DSN 2003: 764

Edmund M. Clarke, Daniel Kroening, Karen Yorav: Specifying and Verifying Systems with Multiple Clocks. ICCD 2003: 48-

Samir Sapra, Michael Theobald, Edmund M. Clarke: SAT-Based Algorithms for Logic Minimization. ICCD 2003: 510-

Sagar Chaki, Edmund M. Clarke, Alex Groce, Somesh Jha, Helmut Veith: Modular Verification of Software Components in C. ICSE 2003: 385-395

Edmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang: High Level Verification of Control Intensive Systems Using Predicate Abstraction. MEMOCODE 2003: 55-64

Edmund M. Clarke, Muralidhar Talupur, Helmut Veith, Dong Wang: SAT Based Predicate Abstraction for Hardware Verification. SAT 2003: 78-92

Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Olaf Stursberg, Michael Theobald: Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. TACAS 2003: 192-207

Edmund M. Clarke: Counterexample-Guided Abstraction Refinement. TIME 2003: 7

Sergey Berezin, Edmund M. Clarke, Armin Biere, Yunshan Zhu: Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function. Formal Methods in System Design 20(2): 159-186 (2002)

Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum: Program slicing for VHDL. STTT 4(1): 125-137 (2002)

Edmund M. Clarke, Anubhav Gupta, James H. Kukula, Ofer Strichman: SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. CAV 2002: 265-279

Alessandro Cimatti, Edmund M. Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. CAV 2002: 359-364

Pankaj Chauhan, Edmund M. Clarke, James H. Kukula, Samir Sapra, Helmut Veith, Dong Wang: Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis. FMCAD 2002: 33-51

Edmund M. Clarke, Somesh Jha, Yuan Lu, Helmut Veith: Tree-Like Counterexamples in Model Checking. LICS 2002: 19-29

Edmund M. Clarke: SAT-Based Counterexample Guided Abstraction Refinement. SPIN 2002: 1

Edmund M. Clarke, Orna Grumberg, Doron Peled: Model checking. MIT Press 2001, isbn 978-0-262-03270-4, pp. I-XIV, 1-314

Edmund M. Clarke, Armin Biere, Richard Raimi, Yunshan Zhu: Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19(1): 7-34 (2001)

Sérgio Vale Aguiar Campos, Edmund M. Clarke: The Verus language: representing time efficiently with BDDs. Theor. Comput. Sci. 253(1): 95-118 (2001)

Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Helmut Veith, Dong Wang: Using Combinatorial Optimization Methods for Quantification Scheduling. CHARME 2001: 293-309

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith: Progress on the State Explosion Problem in Model Checking. Informatics 2001: 176-194

Dong Wang, Edmund M. Clarke, Yunshan Zhu, James H. Kukula: Using cutwidth to improve symbolic simulation and Boolean satisfiability. HLDVT 2001: 165-170

Pankaj Chauhan, Edmund M. Clarke, Somesh Jha, James H. Kukula, Thomas R. Shiple, Helmut Veith, Dong Wang: Non-linear Quantification Scheduling in Image Computation. ICCAD 2001: 293-

Alexis Campailla, Sagar Chaki, Edmund M. Clarke, Somesh Jha, Helmut Veith: Efficient Filtering in Publish-Subscribe Systems Using Binary Decision. ICSE 2001: 443-452

Edmund M. Clarke, Bernd-Holger Schlingloff: Model Checking. Handbook of Automated Reasoning 2001: 1635-1790

Sérgio Vale Aguiar Campos, Edmund M. Clarke, Orna Grumberg: Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. Formal Methods in System Design 17(2): 163-192 (2000)

Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia: Verification of a safety-critical railway interlocking system with real-time constraints. Sci. Comput. Program. 36(1): 53-64 (2000)

Edmund M. Clarke: Automatic verification of hardware and software systems. ACM SIGSOFT Software Engineering Notes 25(1): 41-42 (2000)

Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri: NUSMV: A New Symbolic Model Checker. STTT 2(4): 410-425 (2000)

Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero: Verifying security protocols with Brutus. ACM Trans. Softw. Eng. Methodol. 9(4): 443-487 (2000)

Sergey Berezin, Edmund M. Clarke, Somesh Jha, Will Marrero: Model checking algorithms for the µ-calculus. Proof, Language, and Interaction 2000: 309-338

Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta: Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. CAV 2000: 124-138

Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, Helmut Veith: Counterexample-Guided Abstraction Refinement. CAV 2000: 154-169

Yuan Lu, Jawahar Jain, Edmund M. Clarke, Masahiro Fujita: Efficient variable ordering using aBDD based sampling. DAC 2000: 687-692

Edmund M. Clarke, Steven M. German, Yuan Lu, Helmut Veith, Dong Wang: Executable Protocol Specification in ESL. FMCAD 2000: 197-216

Randal E. Bryant, Pankaj Chauhan, Edmund M. Clarke, Amit Goel: A Theory of Consistency for Modular Synchronous Systems. FMCAD 2000: 486-504

Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero: Partial Order Reductions for Security Protocol Verification. TACAS 2000: 503-518

Christel Baier, Edmund M. Clarke, Vasilili Hartonas-Garmhausen: On the Semantic Foundations of Probabilistic Synchronous Reactive Programs. Electr. Notes Theor. Comput. Sci. 22: 3-28 (1999)

Armin Biere, Edmund M. Clarke, Yunshan Zhu: Combining Local and Global Model Checking. Electr. Notes Theor. Comput. Sci. 23(2): 34-45 (1999)

Sérgio Vale Aguiar Campos, Marcio Teixeira, Marius Minea, Andreas Kuehlmann, Edmund M. Clarke: Model Checking Semi-Continuous Time Models Using BDDs. Electr. Notes Theor. Comput. Sci. 23(2): 75-87 (1999)

Edmund M. Clarke, Steven M. German, Xudong Zhao: Verifying the SRT Division Algorithm Using Theorem Proving Techniques. Formal Methods in System Design 14(1): 7-44 (1999)

Sérgio Vale Aguiar Campos, Edmund M. Clarke: Analysis and Verification of Real-Time Systems Using Quantitative Symbolic Algorithms. STTT 2(3): 260-269 (1999)

Edmund M. Clarke, Orna Grumberg, Marius Minea, Doron Peled: State Space Reduction Using Partial Order Techniques. STTT 2(3): 279-287 (1999)

Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Edmund M. Clarke: ProbVerus: Probabilistic Symbolic Model Checking. ARTS 1999: 96-110

Armin Biere, Edmund M. Clarke, Yunshan Zhu: Multiple State and Single State Tableaux for Combining Local and Global Model Checking. Correct System Design 1999: 163-179

Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu: Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. CAV 1999: 60-71

Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia, Marco Roveri: NUSMV: A New Symbolic Model Verifier. CAV 1999: 495-499

Edmund M. Clarke, Somesh Jha, Yuan Lu, Dong Wang: Abstract BDDs: A Technque for Using Abstraction in Model Checking. CHARME 1999: 172-186

Edmund M. Clarke, Masahiro Fujita, Sreeranga P. Rajan, Thomas W. Reps, Subash Shankar, Tim Teitelbaum: Program Slicing of Hardware Description Languages. CHARME 1999: 298-312

Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Masahiro Fujita, Yunshan Zhu: Symbolic Model Checking Using SAT Procedures instead of BDDs. DAC 1999: 317-320

Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu: Symbolic Model Checking without BDDs. TACAS 1999: 193-207

Andrej Bauer, Edmund M. Clarke, Xudong Zhao: Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation. J. Autom. Reasoning 21(3): 295-325 (1998)

Edmund M. Clarke, E. Allen Emerson, Somesh Jha, A. Prasad Sistla: Symmetry Reductions inModel Checking. CAV 1998: 147-158

Sergey Berezin, Armin Biere, Edmund M. Clarke, Yunshan Zhu: Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. FMCAD 1998: 369-386

David Déharbe, Subash Shankar, Edmund M. Clarke: Model Checking VHDL with CV. FMCAD 1998: 508-514

Vicky Hartonas-Garmhausen, Sérgio Vale Aguiar Campos, Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia: Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints. FTCS 1998: 458-463

Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero: Using state space exploration and a natural deduction style message derivation engine to verify security protocols. PROCOMET 1998: 87-106

Edmund M. Clarke, Sergey Berezin: Model Checking: Historical Perspective and Example (Extended Abstract). TABLEAUX 1998: 18-24

Edmund M. Clarke: Editorial. Formal Methods in System Design 10(1): 5 (1997)

Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi: Another Look at LTL Model Checking. Formal Methods in System Design 10(1): 47-71 (1997)

Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, J. Yang: Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. Formal Methods in System Design 10(2/3): 137-148 (1997)

Sérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea: Symbolic Techniques for Formally Verifying Industrial Systems. Sci. Comput. Program. 29(1-2): 79-98 (1997)

Anca Browne, Edmund M. Clarke, Somesh Jha, David E. Long, Wilfredo R. Marrero: An Improved Algorithm for the Evaluation of Fixpoint Expressions. Theor. Comput. Sci. 178(1-2): 237-255 (1997)

Edmund M. Clarke, Orna Grumberg, Somesh Jha: Verifying Parameterized Networks. ACM Trans. Program. Lang. Syst. 19(5): 726-750 (1997)

Sérgio Vale Aguiar Campos, Edmund M. Clarke: The Verus Language: Representing Time Efficiently with BDDs. ARTS 1997: 64-78

Sérgio Vale Aguiar Campos, Edmund M. Clarke, Marius Minea: The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems. CAV 1997: 452-455

Sergey Berezin, Sérgio Vale Aguiar Campos, Edmund M. Clarke: Compositional Reasoning in Model Checking. COMPOS 1997: 81-102

Edmund M. Clarke: Model Cheking. FSTTCS 1997: 54-56

Christel Baier, Edmund M. Clarke, Vassili Hartonas-Garmhausen, Marta Z. Kwiatkowska, Mark Ryan: Symbolic Model Checking for Probabilistic Processes. ICALP 1997: 430-440

Somesh Jha, Yuan Lu, Marius Minea, Edmund M. Clarke: Equivalence Checking Using Abstract BDDs. ICCD 1997: 332-337

Edmund M. Clarke: Temporal Logic Model Checking (Abstract). ILPS 1997: 3

Edmund M. Clarke, Jeannette M. Wing: Tools and Partial Analysis. ACM Comput. Surv. 28(4es): 116 (1996)

Edmund M. Clarke, Jeannette M. Wing: Formal Methods: State of the Art and Future Directions. ACM Comput. Surv. 28(4): 626-643 (1996)

Edmund M. Clarke, Somesh Jha, Reinhard Enders, Thomas Filkorn: Exploiting Symmetry in Temporal Logic Model Checking. Formal Methods in System Design 9(1/2): 77-104 (1996)

Andrej Bauer, Edmund M. Clarke, Xudong Zhao: Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation. AISMC 1996: 21-37

Edmund M. Clarke, Steven M. German, Xudong Zhao: Verifying the SRT Division Algorithm Using Theorem Proving Techniques. CAV 1996: 111-122

Edmund M. Clarke, Kenneth L. McMillan, Sérgio Vale Aguiar Campos, Vassili Hartonas-Garmhausen: Symbolic Model Checking. CAV 1996: 419-427

Edmund M. Clarke, Manpreet Khaira, Xudong Zhao: Word Level Model Checking - Avoiding the Pentium FDIV Error. DAC 1996: 645-648

Yirng-An Chen, Edmund M. Clarke, Pei-Hsin Ho, Yatin Vasant Hoskote, Timothy Kam, Manpreet Khaira, John W. O'Leary, Xudong Zhao: Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking. FMCAD 1996: 19-33

Vasilili Hartonas-Garmhausen, Edmund M. Clarke, S. Campos: Deadlock prevention in flexible manufacturing systems using symbolic model checking. ICRA 1996: 527-532

Edmund M. Clarke, Xudong Zhao: Word Level Model Checking (Abstract). MFCS 1996: 1

Edmund M. Clarke, Orna Grumberg, David E. Long: Model checking. NATO ASI DPD 1996: 305-349

Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness: Verification of the Futurebus+ Cache Coherence Protocol. Formal Methods in System Design 6(2): 217-232 (1995)

Sérgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea, Hiromi Hiraishi: Temporal Verification of Real-Time Systems. IEICE Transactions 78-D(7): 796-801 (1995)

Edmund M. Clarke, Orna Grumberg, Somesh Jha: Veryfying Parameterized Networks using Abstraction and Regular Languages. CONCUR 1995: 395-407

Edmund M. Clarke, Orna Grumberg, Kenneth L. McMillan, Xudong Zhao: Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC 1995: 427-432

Edmund M. Clarke, Masahiro Fujita, Xudong Zhao: Hybrid decision diagrams. ICCAD 1995: 159-163

Sérgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea: Verifying the performance of the PCI local bus using symbolic techniques. ICCD 1995: 72-78

Sérgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea: Verus: A Tool for Quantitative Analysis of Finite-State Real-Time Systems. Workshop on Languages, Compilers, & Tools for Real-Time Systems 1995: 70-78

Edmund M. Clarke, Somesh Jha: Symmetry and Induction in Model Checking. Computer Science Today 1995: 455-470

Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, David L. Dill: Symbolic model checking for sequential circuit verification. IEEE Trans. on CAD of Integrated Circuits and Systems 13(4): 401-424 (1994)

Edmund M. Clarke, Orna Grumberg, David E. Long: Model Checking and Abstraction. ACM Trans. Program. Lang. Syst. 16(5): 1512-1542 (1994)

Edmund M. Clarke: Automatic Verification of Finite-state Concurrent Systems. Application and Theory of Petri Nets 1994: 1

Edmund M. Clarke, Xudong Zhao: Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan. CADE 1994: 758-763

David E. Long, Anca Browne, Edmund M. Clarke, Somesh Jha, Wilfredo R. Marrero: An Improved Algorithm for the Evaluation of Fixpoint Expressions. CAV 1994: 338-350

Edmund M. Clarke, Orna Grumberg, Kiyoharu Hamaguchi: Another Look at LTL Model Checking. CAV 1994: 415-427

Masahiro Fujita, Jerry Chih-Yuan Yang, Edmund M. Clarke, Xudong Zhao, Patrick C. McGeer: Fast Spectrum Computation for Logic Functions using Binary Decision Diagrams. ISCAS 1994: 275-278

Edmund M. Clarke: Automatic Verification of Finite-State Concurrent Systems. LICS 1994: 126

Sérgio Vale Aguiar Campos, Edmund M. Clarke, Wilfredo R. Marrero, Marius Minea, Hiromi Hiraishi: Computing Quantitative Characteristics of Finite-State Real-Time Systems. RTSS 1994: 266-270

Frank D. Anger, Edmund M. Clarke: New and used temporal models: An issue of time. Appl. Intell. 3(1): 5-15 (1993)

Edmund M. Clarke, I. A. Draghicescu, Robert P. Kurshan: A Unified Approch for Showing Language Inclusion and Equivalence Between Various Types of omega-Automata. Inf. Process. Lett. 46(6): 301-308 (1993)

Tomohiro Yoneda, Atsufumi Shibayama, Bernd-Holger Schlingloff, Edmund M. Clarke: Efficient Verification of Parallel Real-Time Systems. CAV 1993: 321-346

Edmund M. Clarke, Thomas Filkorn, Somesh Jha: Exploiting Symmetry In Temporal Logic Model Checking. CAV 1993: 450-462

Edmund M. Clarke, Orna Grumberg, Hiromi Hiraishi, Somesh Jha, David E. Long, Kenneth L. McMillan, Linda A. Ness: Verification of the Futurebus+ Cache Coherence Protocol. CHDL 1993: 15-30

Edmund M. Clarke: Automatic Verification of Sequential Circuit Designs. CHDL 1993: 165

Edmund M. Clarke, Kenneth L. McMillan, Xudong Zhao, Masahiro Fujita, J. Yang: Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. DAC 1993: 54-60

Edmund M. Clarke, Orna Grumberg, David E. Long: Verification Tools for Finite-State Concurrent Systems. REX School/Symposium 1993: 124-175

Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang: Symbolic Model Checking: 10^20 States and Beyond. Inf. Comput. 98(2): 142-170 (1992)

Soumitra Bose, Edmund M. Clarke, David E. Long, Spiro Michaylov: PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. J. Autom. Reasoning 8(2): 153-181 (1992)

Edmund M. Clarke, Orna Grumberg, Robert P. Kurshan: A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. J. Log. Comput. 2(5): 605-618 (1992)

Edmund M. Clarke, Xudong Zhao: Analytica - A Theorem Prover in Mathematica. CADE 1992: 761-765

Edmund M. Clarke, Orna Grumberg, David E. Long: Model Checking and Abstraction. POPL 1992: 342-354

Jerry R. Burch, Edmund M. Clarke, David E. Long: Representing Circuits More Efficiently in Symbolic Model Checking. DAC 1991: 403-407

Jerry R. Burch, Edmund M. Clarke, David E. Long: Symbolic Model Checking with Partitioned Transistion Relations. VLSI 1991: 49-58

Edmund M. Clarke, Robert P. Kurshan (Eds.): Computer Aided Verification, 2nd International Workshop, CAV '90, New Brunswick, NJ, USA, June 18-21, 1990, Proceedings. Lecture Notes in Computer Science 531, Springer 1991, isbn 3-540-54477-1

Edmund M. Clarke, Anca Browne, Robert P. Kurshan: A Unified Approach For Showing Language Containment And Equivalence Between Various Types Of Omega-Automata. CAAP 1990: 103-116

Edmund M. Clarke: Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem. CAV 1990: 1

Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill: Sequential Circuit Verification Using Symbolic Model Checking. DAC 1990: 46-51

Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, L. J. Hwang: Symbolic Model Checking: 10^20 States and Beyond. LICS 1990: 428-439

Michael C. Browne, Edmund M. Clarke, Orna Grumberg: Reasoning about Networks with Many Identical Finite State Processes. Inf. Comput. 81(1): 13-31 (1989)

Steven M. German, Edmund M. Clarke, Joseph Y. Halpern: Reasoning about Procedures as Parameters in the Language L4. Inf. Comput. 83(3): 265-359 (1989)

Edmund M. Clarke, Orna Grumberg, Robert P. Kurshan: A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. Logic at Botik 1989: 81-90

Soumitra Bose, Edmund M. Clarke, David E. Long, Spiro Michaylov: PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. LICS 1989: 80-89

Edmund M. Clarke, David E. Long, Kenneth L. McMillan: Compositional Model Checking. LICS 1989: 353-362

Edmund M. Clarke, Yulin Feng: Escher-a geometrical layout system for recursively defined circuits. IEEE Trans. on CAD of Integrated Circuits and Systems 7(8): 908-918 (1988)

Michael C. Browne, Edmund M. Clarke, Orna Grumberg: Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theor. Comput. Sci. 59: 115-131 (1988)

P. E. Allen, Soumitra Bose, Edmund M. Clarke, Spiro Michaylov: PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. CADE 1988: 764-765

Edmund M. Clarke, I. A. Draghicescu: Expressibility results for linear-time and branching-time logics. REX Workshop 1988: 428-437

Edmund M. Clarke, Orna Grumberg: Avoiding The State Explosion Problem in Temporal Logic Model Checking. PODC 1987: 294-303

Michael C. Browne, Edmund M. Clarke, Orna Grumberg: Characterizing Kripke Structures in Temporal Logic. TAPSOFT, Vol.1 1987: 256-270

Edmund M. Clarke, Orna Grumberg: The Model Checking Problem for Concurrent Systems with Many Similar Processes. Temporal Logic in Specification 1987: 188-201

Thomas S. Anantharaman, Edmund M. Clarke, Michael J. Foster, Bud Mishra: Compiling Path Expressions Into VLSI Circuits. Distributed Computing 1(3): 150-166 (1986)

Edmund M. Clarke: Distributed Computing Issues in Hardware Design. Distributed Computing 1(4): 185-186 (1986)

Michael C. Browne, Edmund M. Clarke, David L. Dill, Bud Mishra: Automatic Verification of Sequential Circuits Using Temporal Logic. IEEE Trans. Computers 35(12): 1035-1044 (1986)

Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst. 8(2): 244-263 (1986)

Edmund M. Clarke, Yulin Feng: Escher - a geometrical layout system for recursively defined circuits. DAC 1986: 650-653

Steven M. German, Edmund M. Clarke, Joseph Y. Halpern: True Relative Completeness of an Axiom System for the Language L4 (Abridged). LICS 1986: 11-25

Edmund M. Clarke, Orna Grumberg, Michael C. Browne: Reasoning About Networks With Many Identical Finite-State Processes. PODC 1986: 240-248

A. Prasad Sistla, Edmund M. Clarke: The Complexity of Propositional Linear Temporal Logics. J. ACM 32(3): 733-749 (1985)

Bhubaneswaru Mishra, Edmund M. Clarke: Hierarchical Verification of Asynchronous Circuits Using Temporal Logic. Theor. Comput. Sci. 38: 269-291 (1985)

Thomas S. Anantharaman, Edmund M. Clarke, Michael J. Foster, Bud Mishra: Compiling Path Expressions into VLSI Circuits. POPL 1985: 191-204

A. Prasad Sistla, Edmund M. Clarke, Nissim Francez, Albert R. Meyer: Can Message Buffers Be Axiomatized in Linear Temporal Logic? Information and Control 63(1/2): 88-112 (1984)

Edmund M. Clarke, Dexter Kozen (Eds.): Logics of Programs, Workshop, Carnegie Mellon University, Pittsburgh, PA, USA, June 6-8, 1983, Proceedings. Lecture Notes in Computer Science 164, Springer 1984, isbn 3-540-12896-4

Edmund M. Clarke, Steven M. German, Joseph Y. Halpern: Effective Axiomatizations of Hoare Logics. J. ACM 30(3): 612-636 (1983)

Edmund M. Clarke, Bud Mishra: Automatic Verification of Asynchronous Circuits. Logic of Programs 1983: 101-115

Steven M. German, Edmund M. Clarke, Joseph Y. Halpern: Reasoning About Procedures as Parameters. Logic of Programs 1983: 206-220

Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla: Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. POPL 1983: 117-126

E. Allen Emerson, Edmund M. Clarke: Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Sci. Comput. Program. 2(3): 241-266 (1982)

Edmund M. Clarke, Christos Nikolaou: Distributed Reconfiguration Strategies for Fault-Tolerant Multiprocessor Systems. IEEE Trans. Computers 31(8): 771-784 (1982)

A. Prasad Sistla, Edmund M. Clarke, Nissim Francez, Yuri Gurevich: Can Message Buffers be Characterized in Linear Temporal Logic? PODC 1982: 148-156

Edmund M. Clarke, Steven M. German, Joseph Y. Halpern: On Effective Axiomatizations of Hoare Logics. POPL 1982: 309-321

A. Prasad Sistla, Edmund M. Clarke: The Complexity of Propositional Linear Temporal Logics. STOC 1982: 159-168

Eric S. Roberts, Arthur Evans Jr., C. Robert Morgan, Edmund M. Clarke: Task Management in Ada-A Critical Evaluation for Real-time Multiprocessors. Softw., Pract. Exper. 11(10): 1019-1051 (1981)

Edmund M. Clarke, E. Allen Emerson: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logic of Programs 1981: 52-71

Edmund M. Clarke: Proving Correctness of Coroutines Without History Variables. Acta Inf. 13: 169-188 (1980)

Edmund M. Clarke: Synthesis of Resource Invariants for Concurrent Programs. ACM Trans. Program. Lang. Syst. 2(3): 338-358 (1980)

E. Allen Emerson, Edmund M. Clarke: Characterizing Correctness Properties of Parallel Programs Using Fixpoints. ICALP 1980: 169-181

Philip A. Bernstein, Barbara T. Blaustein, Edmund M. Clarke: Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data. VLDB 1980: 126-136

Edmund M. Clarke: Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems. J. ACM 26(1): 129-147 (1979)

Edmund M. Clarke, Lishing Liu: Approximate Algorithms for Optimization of Busy Waiting in Parallel Programs (Preliminary Report). FOCS 1979: 255-266

Edmund M. Clarke: Synthesis of Resource Invariants for Concurrent Programs. POPL 1979: 211-221

Edmund M. Clarke: Program Invariants as Fixed Points (Preliminary Reports). FOCS 1977: 18-29

Edmund M. Clarke: Programming Language Constructs for Which it is Impossible to Obtain "Good" Hoare-Like Axiom Systems. POPL 1977: 10-20