| 2009 |
|---|
| 221 | EE | 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 |
| 2008 |
|---|
| 220 | EE | Edmund M. Clarke:
The Birth of Model Checking.
25 Years of Model Checking 2008: 1-26 |
| 219 | EE | 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 |
| 218 | EE | André Platzer,
Edmund M. Clarke:
Computing Differential Invariants of Hybrid Systems as Fixedpoints.
CAV 2008: 176-189 |
| 217 | EE | Himanshu Jain,
Edmund M. Clarke,
Orna Grumberg:
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations.
CAV 2008: 254-267 |
| 216 | EE | 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 |
| 215 | EE | Flavio Lerda,
James Kapinski,
Edmund M. Clarke,
Bruce H. Krogh:
Verification of Supervisory Control Software Using State Proximity and Merging.
HSCC 2008: 344-357 |
| 214 | EE | 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 |
| 213 | EE | Edmund M. Clarke:
Model Checking - My 27-Year Quest to Overcome the State Explosion Problem.
LPAR 2008: 182 |
| 212 | EE | 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 |
| 211 | EE | Edmund M. Clarke,
Muralidhar Talupur,
Helmut Veith:
Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems.
TACAS 2008: 33-47 |
| 210 | EE | 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) |
| 209 | EE | 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) |
| 2007 |
|---|
| 208 | EE | Nishant Sinha,
Edmund M. Clarke:
SAT-Based Compositional Verification Using Lazy Learning.
CAV 2007: 39-54 |
| 207 | EE | 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 |
| 206 | EE | André Platzer,
Edmund M. Clarke:
The Image Computation Problem in Hybrid Systems Model Checking.
HSCC 2007: 473-486 |
| 205 | EE | Stephen Magill,
Josh Berdine,
Edmund M. Clarke,
Byron Cook:
Arithmetic Strengthening for Shape Analysis.
SAS 2007: 419-436 |
| 204 | EE | Himanshu Jain,
Daniel Kroening,
Natasha Sharygina,
Edmund M. Clarke:
VCEGAR: Verilog CounterExample Guided Abstraction Refinement.
TACAS 2007: 583-586 |
| 203 | EE | Edmund M. Clarke,
Himanshu Jain,
Daniel Kroening:
Verification of SpecC using predicate abstraction.
Formal Methods in System Design 30(1): 5-28 (2007) |
| 202 | EE | Edmund M. Clarke,
Flavio Lerda:
Model Checking: Software and Beyond.
J. UCS 13(5): 639-649 (2007) |
| 2006 |
|---|
| 201 | | Edmund M. Clarke,
Marius Minea,
Ferucio Laurentiu Tiplea:
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
IOS Press 2006 |
| 200 | EE | Vaibhav Mehta,
Constantinos Bartzis,
Haifeng Zhu,
Edmund M. Clarke,
Jeannette M. Wing:
Ranking Attack Graphs.
RAID 2006: 127-144 |
| 199 | EE | Himanshu Jain,
Constantinos Bartzis,
Edmund M. Clarke:
Satisfiability Checking of Non-clausal Formulas Using General Matings.
SAT 2006: 75-89 |
| 198 | EE | 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 |
| 197 | EE | Edmund M. Clarke,
Muralidhar Talupur,
Helmut Veith:
Environment Abstraction for Parameterized Verification.
VMCAI 2006: 126-141 |
| 2005 |
|---|
| 196 | EE | Sagar Chaki,
Edmund M. Clarke,
Nishant Sinha,
Prasanna Thati:
Automated Assume-Guarantee Reasoning for Simulation Conformance.
CAV 2005: 534-547 |
| 195 | EE | Himanshu Jain,
Daniel Kroening,
Natasha Sharygina,
Edmund M. Clarke:
Word level predicate abstraction and refinement for verifying RTL verilog.
DAC 2005: 445-450 |
| 194 | EE | Natasha Sharygina,
Sagar Chaki,
Edmund M. Clarke,
Nishant Sinha:
Dynamic Component Substitutability Analysis.
FM 2005: 512-528 |
| 193 | EE | Edmund M. Clarke,
Natasha Sharygina,
Nishant Sinha:
Program Compatibility Approaches.
FMCO 2005: 243-258 |
| 192 | EE | Ansgar Fehnker,
Edmund M. Clarke,
Sumit Kumar Jha,
Bruce H. Krogh:
Refining Abstractions of Hybrid Systems Using Counterexample Fragments.
HSCC 2005: 242-257 |
| 191 | EE | Anubhav Gupta,
Edmund M. Clarke:
Reconsidering CEGAR: Learning Good Abstractions without Refinement.
ICCD 2005: 591-598 |
| 190 | EE | 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 |
| 189 | EE | Edmund M. Clarke,
Daniel Kroening,
Natasha Sharygina,
Karen Yorav:
SATABS: SAT-Based Predicate Abstraction for ANSI-C.
TACAS 2005: 570-574 |
| 188 | | Edmund M. Clarke,
Himanshu Jain,
Nishant Sinha:
Grand Challenge: Model Check Software.
VISSAS 2005: 55-68 |
| 187 | EE | Edmund M. Clarke,
Anubhav Gupta,
Himanshu Jain,
Helmut Veith:
Model Checking: Back and Forth between Hardware and Software.
VSTTE 2005: 251-255 |
| 186 | | Edmund M. Clarke,
Ansgar Fehnker,
Sumit Kumar Jha,
Helmut Veith:
Temporal Logic Model Checking.
Handbook of Networked and Embedded Control Systems 2005: 539-558 |
| 185 | EE | 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) |
| 184 | EE | Sagar Chaki,
Edmund M. Clarke,
Somesh Jha,
Helmut Veith:
An Iterative Framework for Simulation Conformance.
J. Log. Comput. 15(4): 465-488 (2005) |
| 183 | EE | Edmund M. Clarke,
Daniel Kroening,
Joël Ouaknine,
Ofer Strichman:
Computational challenges in bounded model checking.
STTT 7(2): 174-183 (2005) |
| 2004 |
|---|
| 182 | EE | Edmund M. Clarke,
Muralidhar Talupur,
Tayssir Touili,
Helmut Veith:
Verification by Network Decomposition.
CONCUR 2004: 276-291 |
| 181 | EE | Pankaj Chauhan,
Edmund M. Clarke,
Daniel Kroening:
A SAT-based algorithm for reparameterization in symbolic simulation.
DAC 2004: 524-529 |
| 180 | EE | Daniel Kroening,
Edmund M. Clarke:
Checking consistency of C and Verilog using predicate abstraction and induction.
ICCAD 2004: 66-72 |
| 179 | EE | Daniel Kroening,
Alex Groce,
Edmund M. Clarke:
Counterexample Guided Abstraction Refinement Via Program Execution.
ICFEM 2004: 224-238 |
| 178 | EE | Edmund M. Clarke,
Daniel Kroening:
Tutorial: Software Model Checking.
ICFEM 2004: 9-10 |
| 177 | EE | Sagar Chaki,
Edmund M. Clarke,
Joël Ouaknine,
Natasha Sharygina,
Nishant Sinha:
State/Event-Based Software Model Checking.
IFM 2004: 128-147 |
| 176 | EE | Sagar Chaki,
Edmund M. Clarke,
Joël Ouaknine,
Natasha Sharygina:
Automated, compositional and iterative deadlock detection.
MEMOCODE 2004: 201-210 |
| 175 | EE | Himanshu Jain,
Daniel Kroening,
Edmund M. Clarke:
Verification of SpecC using predicate abstraction.
MEMOCODE 2004: 7-16 |
| 174 | EE | Edmund M. Clarke,
Daniel Kroening,
Flavio Lerda:
A Tool for Checking ANSI-C Programs.
TACAS 2004: 168-176 |
| 173 | EE | Edmund M. Clarke,
Daniel Kroening,
Joël Ouaknine,
Ofer Strichman:
Completeness and Complexity of Bounded Model Checking.
VMCAI 2004: 85-96 |
| 172 | EE | 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) |
| 171 | EE | 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) |
| 170 | EE | 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) |
| 169 | EE | 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) |
| 168 | EE | 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) |
| 2003 |
|---|
| 167 | EE | Edmund M. Clarke:
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking.
CADE 2003: 1 |
| 166 | EE | Edmund M. Clarke,
Orna Grumberg,
Muralidhar Talupur,
Dong Wang:
Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates.
CAV 2003: 126-140 |
| 165 | EE | Sagar Chaki,
Edmund M. Clarke,
Alex Groce,
Ofer Strichman:
Predicate Abstraction with Minimum Predicates.
CHARME 2003: 19-34 |
| 164 | EE | Edmund M. Clarke,
Daniel Kroening,
Karen Yorav:
Behavioral consistency of C and verilog programs using bounded model checking.
DAC 2003: 368-371 |
| 163 | EE | Edmund M. Clarke,
Masahiro Fujita,
David P. Gluch:
Model Checking for Dependable Software-Intensive Systems.
DSN 2003: 764 |
| 162 | EE | Edmund M. Clarke,
Daniel Kroening,
Karen Yorav:
Specifying and Verifying Systems with Multiple Clocks.
ICCD 2003: 48- |
| 161 | EE | Samir Sapra,
Michael Theobald,
Edmund M. Clarke:
SAT-Based Algorithms for Logic Minimization.
ICCD 2003: 510- |
| 160 | EE | Sagar Chaki,
Edmund M. Clarke,
Alex Groce,
Somesh Jha,
Helmut Veith:
Modular Verification of Software Components in C.
ICSE 2003: 385-395 |
| 159 | EE | Edmund M. Clarke,
Orna Grumberg,
Muralidhar Talupur,
Dong Wang:
High Level Verification of Control Intensive Systems Using Predicate Abstraction.
MEMOCODE 2003: 55-64 |
| 158 | EE | Edmund M. Clarke,
Muralidhar Talupur,
Helmut Veith,
Dong Wang:
SAT Based Predicate Abstraction for Hardware Verification.
SAT 2003: 78-92 |
| 157 | EE | 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 |
| 156 | EE | Edmund M. Clarke:
Counterexample-Guided Abstraction Refinement.
TIME 2003: 7 |
| 155 | EE | Edmund M. Clarke,
Helmut Veith:
Counterexamples Revisited: Principles, Algorithms, Applications.
Verification: Theory and Practice 2003: 208-224 |
| 154 | | Armin Biere,
Alessandro Cimatti,
Edmund M. Clarke,
Ofer Strichman,
Yunshan Zhu:
Bounded model checking.
Advances in Computers 58: 118-149 (2003) |
| 153 | EE | 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): (2003) |
| 152 | EE | 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) |
| 151 | EE | 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) |
| 150 | EE | Edmund M. Clarke,
Somesh Jha,
Wilfredo R. Marrero:
Efficient verification of security protocols using partial-order reductions.
STTT 4(2): 173-188 (2003) |
| 2002 |
|---|
| 149 | EE | Edmund M. Clarke,
Anubhav Gupta,
James H. Kukula,
Ofer Strichman:
SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques.
CAV 2002: 265-279 |
| 148 | EE | 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 |
| 147 | EE | 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 |
| 146 | EE | Edmund M. Clarke,
Somesh Jha,
Yuan Lu,
Helmut Veith:
Tree-Like Counterexamples in Model Checking.
LICS 2002: 19-29 |
| 145 | EE | Edmund M. Clarke:
SAT-Based Counterexample Guided Abstraction Refinement.
SPIN 2002: 1 |
| 144 | | 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) |
| 143 | EE | 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) |
| 2001 |
|---|
| 142 | EE | 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 |
| 141 | EE | 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- |
| 140 | | Alexis Campailla,
Sagar Chaki,
Edmund M. Clarke,
Somesh Jha,
Helmut Veith:
Efficient Filtering in Publish-Subscribe Systems Using Binary Decision.
ICSE 2001: 443-452 |
| 139 | EE | Edmund M. Clarke,
Orna Grumberg,
Somesh Jha,
Yuan Lu,
Helmut Veith:
Progress on the State Explosion Problem in Model Checking.
Informatics 2001: 176-194 |
| 138 | | Edmund M. Clarke,
Bernd-Holger Schlingloff:
Model Checking.
Handbook of Automated Reasoning 2001: 1635-1790 |
| 137 | | 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) |
| 136 | EE | Sérgio Vale Aguiar Campos,
Edmund M. Clarke:
The Verus language: representing time efficiently with BDDs.
Theor. Comput. Sci. 253(1): 95-118 (2001) |
| 2000 |
|---|
| 135 | | 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 |
| 134 | | Edmund M. Clarke,
Orna Grumberg,
Somesh Jha,
Yuan Lu,
Helmut Veith:
Counterexample-Guided Abstraction Refinement.
CAV 2000: 154-169 |
| 133 | EE | Yuan Lu,
Jawahar Jain,
Edmund M. Clarke,
Masahiro Fujita:
Efficient variable ordering using aBDD based sampling.
DAC 2000: 687-692 |
| 132 | EE | Edmund M. Clarke,
Steven M. German,
Yuan Lu,
Helmut Veith,
Dong Wang:
Executable Protocol Specification in ESL.
FMCAD 2000: 197-216 |
| 131 | EE | Randal E. Bryant,
Pankaj Chauhan,
Edmund M. Clarke,
Amit Goel:
A Theory of Consistency for Modular Synchronous Systems.
FMCAD 2000: 486-504 |
| 130 | | Sergey Berezin,
Edmund M. Clarke,
Somesh Jha,
Will Marrero:
Model checking algorithms for the µ-calculus.
Proof, Language, and Interaction 2000: 309-338 |
| 129 | EE | Edmund M. Clarke,
Somesh Jha,
Wilfredo R. Marrero:
Partial Order Reductions for Security Protocol Verification.
TACAS 2000: 503-518 |
| 128 | EE | Edmund M. Clarke,
Somesh Jha,
Wilfredo R. Marrero:
Verifying security protocols with Brutus.
ACM Trans. Softw. Eng. Methodol. 9(4): 443-487 (2000) |
| 127 | | 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) |
| 126 | EE | Alessandro Cimatti,
Edmund M. Clarke,
Fausto Giunchiglia,
Marco Roveri:
NUSMV: A New Symbolic Model Checker.
STTT 2(4): 410-425 (2000) |
| 125 | | 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) |
| 1999 |
|---|
| 124 | EE | Vicky Hartonas-Garmhausen,
Sérgio Vale Aguiar Campos,
Edmund M. Clarke:
ProbVerus: Probabilistic Symbolic Model Checking.
ARTS 1999: 96-110 |
| 123 | EE | Alessandro Cimatti,
Edmund M. Clarke,
Fausto Giunchiglia,
Marco Roveri:
NUSMV: A New Symbolic Model Verifier.
CAV 1999: 495-499 |
| 122 | EE | 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 |
| 121 | EE | Edmund M. Clarke,
Somesh Jha,
Yuan Lu,
Dong Wang:
Abstract BDDs: A Technque for Using Abstraction in Model Checking.
CHARME 1999: 172-186 |
| 120 | EE | 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 |
| 119 | EE | 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 |
| 118 | EE | Armin Biere,
Alessandro Cimatti,
Edmund M. Clarke,
Masahiro Fujita,
Yunshan Zhu:
Symbolic Model Checking Using SAT Procedures instead of BDDs.
DAC 1999: 317-320 |
| 117 | EE | Armin Biere,
Alessandro Cimatti,
Edmund M. Clarke,
Yunshan Zhu:
Symbolic Model Checking without BDDs.
TACAS 1999: 193-207 |
| 116 | EE | Christel Baier,
Edmund M. Clarke,
Vasilili Hartonas-Garmhausen:
On the Semantic Foundations of Probabilistic Synchronous Reactive Programs.
Electr. Notes Theor. Comput. Sci. 22: (1999) |
| 115 | EE | Armin Biere,
Edmund M. Clarke,
Yunshan Zhu:
Combining Local and Global Model Checking.
Electr. Notes Theor. Comput. Sci. 23(2): (1999) |
| 114 | EE | 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): (1999) |
| 113 | | 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) |
| 112 | EE | 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) |
| 111 | EE | Edmund M. Clarke,
Orna Grumberg,
Marius Minea,
Doron Peled:
State Space Reduction Using Partial Order Techniques.
STTT 2(3): 279-287 (1999) |
| 1998 |
|---|
| 110 | | Edmund M. Clarke,
E. Allen Emerson,
Somesh Jha,
A. Prasad Sistla:
Symmetry Reductions inModel Checking.
CAV 1998: 147-158 |
| 109 | EE | 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 |
| 108 | EE | David Déharbe,
Subash Shankar,
Edmund M. Clarke:
Model Checking VHDL with CV.
FMCAD 1998: 508-514 |
| 107 | | 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 |
| 106 | | 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 |
| 105 | EE | Edmund M. Clarke,
Sergey Berezin:
Model Checking: Historical Perspective and Example (Extended Abstract).
TABLEAUX 1998: 18-24 |
| 104 | | 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) |
| 1997 |
|---|
| 103 | | Sérgio Vale Aguiar Campos,
Edmund M. Clarke:
The Verus Language: Representing Time Efficiently with BDDs.
ARTS 1997: 64-78 |
| 102 | | 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 |
| 101 | EE | Sergey Berezin,
Sérgio Vale Aguiar Campos,
Edmund M. Clarke:
Compositional Reasoning in Model Checking.
COMPOS 1997: 81-102 |
| 100 | EE | Edmund M. Clarke:
Model Cheking.
FSTTCS 1997: 54-56 |
| 99 | | Christel Baier,
Edmund M. Clarke,
Vassili Hartonas-Garmhausen,
Marta Z. Kwiatkowska,
Mark Ryan:
Symbolic Model Checking for Probabilistic Processes.
ICALP 1997: 430-440 |
| 98 | | Somesh Jha,
Yuan Lu,
Marius Minea,
Edmund M. Clarke:
Equivalence Checking Using Abstract BDDs.
ICCD 1997: 332-337 |
| 97 | | Edmund M. Clarke:
Temporal Logic Model Checking (Abstract).
ILPS 1997: 3 |
| 96 | EE | Edmund M. Clarke,
Orna Grumberg,
Somesh Jha:
Verifying Parameterized Networks.
ACM Trans. Program. Lang. Syst. 19(5): 726-750 (1997) |
| 95 | | Edmund M. Clarke,
Orna Grumberg,
Kiyoharu Hamaguchi:
Another Look at LTL Model Checking.
Formal Methods in System Design 10(1): 47-71 (1997) |
| 94 | | Edmund M. Clarke:
Editorial.
Formal Methods in System Design 10(1): 5 (1997) |
| 93 | | 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) |
| 92 | | 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) |
| 91 | EE | 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) |
| 1996 |
|---|
| 90 | | Andrej Bauer,
Edmund M. Clarke,
Xudong Zhao:
Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation.
AISMC 1996: 21-37 |
| 89 | | Edmund M. Clarke,
Steven M. German,
Xudong Zhao:
Verifying the SRT Division Algorithm Using Theorem Proving Techniques.
CAV 1996: 111-122 |
| 88 | | Edmund M. Clarke,
Kenneth L. McMillan,
Sérgio Vale Aguiar Campos,
Vassili Hartonas-Garmhausen:
Symbolic Model Checking.
CAV 1996: 419-427 |
| 87 | EE | Edmund M. Clarke,
Manpreet Khaira,
Xudong Zhao:
Word Level Model Checking - Avoiding the Pentium FDIV Error.
DAC 1996: 645-648 |
| 86 | | 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 |
| 85 | | Edmund M. Clarke,
Xudong Zhao:
Word Level Model Checking (Abstract).
MFCS 1996: 1 |
| 84 | | Edmund M. Clarke,
Orna Grumberg,
David E. Long:
Model checking.
NATO ASI DPD 1996: 305-349 |
| 83 | | Edmund M. Clarke,
Jeannette M. Wing:
Formal Methods: State of the Art and Future Directions.
ACM Comput. Surv. 28(4): 626-643 (1996) |
| 82 | | Edmund M. Clarke,
Jeannette M. Wing:
Tools and Partial Analysis.
ACM Comput. Surv. 28(4es): 116 (1996) |
| 81 | | 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) |
| 1995 |
|---|
| 80 | | Edmund M. Clarke,
Orna Grumberg,
Somesh Jha:
Veryfying Parameterized Networks using Abstraction and Regular Languages.
CONCUR 1995: 395-407 |
| 79 | EE | Edmund M. Clarke,
Orna Grumberg,
Kenneth L. McMillan,
Xudong Zhao:
Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking.
DAC 1995: 427-432 |
| 78 | EE | Edmund M. Clarke,
Masahiro Fujita,
Xudong Zhao:
Hybrid decision diagrams.
ICCAD 1995: 159-163 |
| 77 | EE | 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 |
| 76 | | 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 |
| 75 | | Edmund M. Clarke,
Somesh Jha:
Symmetry and Induction in Model Checking.
Computer Science Today 1995: 455-470 |
| 74 | | 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) |
| 1994 |
|---|
| 73 | | Edmund M. Clarke:
Automatic Verification of Finite-state Concurrent Systems.
Application and Theory of Petri Nets 1994: 1 |
| 72 | | Edmund M. Clarke,
Xudong Zhao:
Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan.
CADE 1994: 758-763 |
| 71 | | 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 |
| 70 | | Edmund M. Clarke,
Orna Grumberg,
Kiyoharu Hamaguchi:
Another Look at LTL Model Checking.
CAV 1994: 415-427 |
| 69 | | Sérgio Vale Aguiar Campos,
Edmund M. Clarke,
Wilfredo R. Marrero,
Marius Minea,
Hiromi Hiraishi:
Computing Quantitative Characteristics of Finite-State Real-Time Systems.
IEEE Real-Time Systems Symposium 1994: 266-270 |
| 68 | | 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 |
| 67 | | Edmund M. Clarke:
Automatic Verification of Finite-State Concurrent Systems
LICS 1994: 126 |
| 66 | EE | Edmund M. Clarke,
Orna Grumberg,
David E. Long:
Model Checking and Abstraction.
ACM Trans. Program. Lang. Syst. 16(5): 1512-1542 (1994) |
| 65 | EE | 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) |
| 1993 |
|---|
| 64 | | Tomohiro Yoneda,
Atsufumi Shibayama,
Bernd-Holger Schlingloff,
Edmund M. Clarke:
Efficient Verification of Parallel Real-Time Systems.
CAV 1993: 321-346 |
| 63 | | Edmund M. Clarke,
Thomas Filkorn,
Somesh Jha:
Exploiting Symmetry In Temporal Logic Model Checking.
CAV 1993: 450-462 |
| 62 | | 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 |
| 61 | | Edmund M. Clarke:
Automatic Verification of Sequential Circuit Designs.
CHDL 1993: 165 |
| 60 | EE | 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 |
| 59 | | Edmund M. Clarke,
Orna Grumberg,
David E. Long:
Verification Tools for Finite-State Concurrent Systems.
REX School/Symposium 1993: 124-175 |
| 58 | EE | Frank D. Anger,
Edmund M. Clarke:
New and used temporal models: An issue of time.
Appl. Intell. 3(1): 5-15 (1993) |
| 57 | | 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) |
| 1992 |
|---|
| 56 | | Edmund M. Clarke,
Xudong Zhao:
Analytica - A Theorem Prover in Mathematica.
CADE 1992: 761-765 |
| 55 | | Edmund M. Clarke,
Orna Grumberg,
David E. Long:
Model Checking and Abstraction.
POPL 1992: 342-354 |
| 54 | | 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) |
| 53 | | 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) |
| 52 | | 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) |
| 1991 |
|---|
| 51 | | Edmund M. Clarke,
Robert P. Kurshan:
Computer Aided Verification, 2nd International Workshop, CAV '90, New Brunswick, NJ, USA, June 18-21, 1990, Proceedings
Springer 1991 |
| 50 | EE | Jerry R. Burch,
Edmund M. Clarke,
David E. Long:
Representing Circuits More Efficiently in Symbolic Model Checking.
DAC 1991: 403-407 |
| 49 | | Jerry R. Burch,
Edmund M. Clarke,
David E. Long:
Symbolic Model Checking with Partitioned Transistion Relations.
VLSI 1991: 49-58 |
| 1990 |
|---|
| 48 | | 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 |
| 47 | | Edmund M. Clarke:
Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem.
CAV 1990: 1 |
| 46 | EE | Jerry R. Burch,
Edmund M. Clarke,
Kenneth L. McMillan,
David L. Dill:
Sequential Circuit Verification Using Symbolic Model Checking.
DAC 1990: 46-51 |
| 45 | | 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 |
| 1989 |
|---|
| 44 | | Edmund M. Clarke,
David E. Long,
Kenneth L. McMillan:
Compositional Model Checking
LICS 1989: 353-362 |
| 43 | | Soumitra Bose,
Edmund M. Clarke,
David E. Long,
Spiro Michaylov:
PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses
LICS 1989: 80-89 |
| 42 | | 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 |
| 41 | | Michael C. Browne,
Edmund M. Clarke,
Orna Grumberg:
Reasoning about Networks with Many Identical Finite State Processes
Inf. Comput. 81(1): 13-31 (1989) |
| 40 | | 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) |
| 1988 |
|---|
| 39 | | P. E. Allen,
Soumitra Bose,
Edmund M. Clarke,
Spiro Michaylov:
PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses.
CADE 1988: 764-765 |
| 38 | | Edmund M. Clarke,
I. A. Draghicescu:
Expressibility results for linear-time and branching-time logics.
REX Workshop 1988: 428-437 |
| 37 | EE | 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) |
| 36 | | Michael C. Browne,
Edmund M. Clarke,
Orna Grumberg:
Characterizing Finite Kripke Structures in Propositional Temporal Logic.
Theor. Comput. Sci. 59: 115-131 (1988) |
| 1987 |
|---|
| 35 | | Edmund M. Clarke,
Orna Grumberg:
Avoiding The State Explosion Problem in Temporal Logic Model Checking.
PODC 1987: 294-303 |
| 34 | | Michael C. Browne,
Edmund M. Clarke,
Orna Grumberg:
Characterizing Kripke Structures in Temporal Logic.
TAPSOFT, Vol.1 1987: 256-270 |
| 33 | | Edmund M. Clarke,
Orna Grumberg:
The Model Checking Problem for Concurrent Systems with Many Similar Processes.
Temporal Logic in Specification 1987: 188-201 |
| 1986 |
|---|
| 32 | EE | Edmund M. Clarke,
Yulin Feng:
Escher - a geometrical layout system for recursively defined circuits.
DAC 1986: 650-653 |
| 31 | | 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 |
| 30 | | Edmund M. Clarke,
Orna Grumberg,
Michael C. Browne:
Reasoning About Networks With Many Identical Finite-State Processes.
PODC 1986: 240-248 |
| 29 | EE | 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) |
| 28 | | Thomas S. Anantharaman,
Edmund M. Clarke,
Michael J. Foster,
Bud Mishra:
Compiling Path Expressions Into VLSI Circuits.
Distributed Computing 1(3): 150-166 (1986) |
| 27 | | Edmund M. Clarke:
Distributed Computing Issues in Hardware Design.
Distributed Computing 1(4): 185-186 (1986) |
| 26 | | 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) |
| 1985 |
|---|
| 25 | | Thomas S. Anantharaman,
Edmund M. Clarke,
Michael J. Foster,
Bud Mishra:
Compiling Path Expressions into VLSI Circuits.
POPL 1985: 191-204 |
| 24 | EE | A. Prasad Sistla,
Edmund M. Clarke:
The Complexity of Propositional Linear Temporal Logics
J. ACM 32(3): 733-749 (1985) |
| 23 | | Bhubaneswaru Mishra,
Edmund M. Clarke:
Hierarchical Verification of Asynchronous Circuits Using Temporal Logic.
Theor. Comput. Sci. 38: 269-291 (1985) |
| 1984 |
|---|
| 22 | | Edmund M. Clarke,
Dexter Kozen:
Logics of Programs, Workshop, Carnegie Mellon University, Pittsburgh, PA, USA, June 6-8, 1983, Proceedings
Springer 1984 |
| 21 | | 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) |
| 1983 |
|---|
| 20 | | Edmund M. Clarke,
Bud Mishra:
Automatic Verification of Asynchronous Circuits.
Logic of Programs 1983: 101-115 |
| 19 | | Steven M. German,
Edmund M. Clarke,
Joseph Y. Halpern:
Reasoning About Procedures as Parameters.
Logic of Programs 1983: 206-220 |
| 18 | | 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 |
| 17 | EE | Edmund M. Clarke,
Steven M. German,
Joseph Y. Halpern:
Effective Axiomatizations of Hoare Logics
J. ACM 30(3): 612-636 (1983) |
| 1982 |
|---|
| 16 | | A. Prasad Sistla,
Edmund M. Clarke,
Nissim Francez,
Yuri Gurevich:
Can Message Buffers be Characterized in Linear Temporal Logic?
PODC 1982: 148-156 |
| 15 | | Edmund M. Clarke,
Steven M. German,
Joseph Y. Halpern:
On Effective Axiomatizations of Hoare Logics.
POPL 1982: 309-321 |
| 14 | | A. Prasad Sistla,
Edmund M. Clarke:
The Complexity of Propositional Linear Temporal Logics
STOC 1982: 159-168 |
| 13 | | Edmund M. Clarke,
Christos Nikolaou:
Distributed Reconfiguration Strategies for Fault-Tolerant Multiprocessor Systems.
IEEE Trans. Computers 31(8): 771-784 (1982) |
| 12 | | E. Allen Emerson,
Edmund M. Clarke:
Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons.
Sci. Comput. Program. 2(3): 241-266 (1982) |
| 1981 |
|---|
| 11 | | Edmund M. Clarke,
E. Allen Emerson:
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic.
Logic of Programs 1981: 52-71 |
| 10 | | 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) |
| 1980 |
|---|
| 9 | | E. Allen Emerson,
Edmund M. Clarke:
Characterizing Correctness Properties of Parallel Programs Using Fixpoints.
ICALP 1980: 169-181 |
| 8 | EE | Philip A. Bernstein,
Barbara T. Blaustein,
Edmund M. Clarke:
Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data.
VLDB 1980: 126-136 |
| 7 | EE | Edmund M. Clarke:
Synthesis of Resource Invariants for Concurrent Programs.
ACM Trans. Program. Lang. Syst. 2(3): 338-358 (1980) |
| 6 | | Edmund M. Clarke:
Proving Correctness of Coroutines Without History Variables.
Acta Inf. 13: 169-188 (1980) |
| 1979 |
|---|
| 5 | | Edmund M. Clarke,
Lishing Liu:
Approximate Algorithms for Optimization of Busy Waiting in Parallel Programs (Preliminary Report)
FOCS 1979: 255-266 |
| 4 | EE | Edmund M. Clarke:
Synthesis of Resource Invariants for Concurrent Programs.
POPL 1979: 211-221 |
| 3 | EE | Edmund M. Clarke:
Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems.
J. ACM 26(1): 129-147 (1979) |
| 1977 |
|---|
| 2 | | Edmund M. Clarke:
Program Invariants as Fixed Points (Preliminary Reports)
FOCS 1977: 18-29 |
| 1 | | Edmund M. Clarke:
Programming Language Constructs for Which it is Impossible to Obtain "Good" Hoare-Like Axiom Systems.
POPL 1977: 10-20 |
