Edmund M. Clarke Home Page Coauthor index DBLP Vis pubzone.org

List of publications from the DBLP Bibliography Server - FAQ
Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo

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

Coauthor Index

1P. E. Allen [39]
2Thomas S. Anantharaman [25] [28]
3Frank D. Anger [58]
4Christel Baier [99] [116]
5Constantinos Bartzis [199] [200]
6Andrej Bauer [90] [104]
7Josh Berdine [205]
8Sergey Berezin [101] [105] [109] [130] [144]
9Philip A. Bernstein [8]
10Armin Biere [109] [115] [117] [118] [119] [122] [135] [137] [144] [154]
11Barbara T. Blaustein [8]
12Soumitra Bose [39] [43] [53]
13Anca Browne (I. A. Draghicescu) [38] [48] [57] [71] [91]
14Michael C. Browne [26] [30] [34] [36] [41]
15Randal E. Bryant [131]
16Jerry R. Burch [45] [46] [49] [50] [54] [65]
17Alexis Campailla [140]
18Sérgio Vale Aguiar Campos [69] [76] [77] [88] [92] [101] [102] [103] [107] [112] [114] [124] [125] [127] [136]
19Sagar Chaki [140] [153] [160] [165] [169] [170] [176] [177] [184] [185] [190] [194] [196] [198] [210]
20Pankaj Chauhan [131] [141] [142] [147] [181]
21Yirng-An Chen [86]
22Yu-Fang Chen [212] [225]
23Alessandro Cimatti [107] [117] [118] [123] [125] [126] [148] [154]
24Byron Cook [205]
25David Déharbe (David Boris Paul Déharbe) [108]
26David L. Dill [26] [45] [46] [54] [65]
27Alexandre Donzé [214]
28E. Allen Emerson [9] [11] [12] [18] [29] [110] [219] [224]
29Reinhard Enders [81]
30Arthur Evans Jr. [10]
31James R. Faeder [216]
32Marcia Falcão [172]
33Azadeh Farzan [212] [225]
34Ansgar Fehnker [152] [157] [186] [192]
35Yulin Feng [32] [37]
36Thomas Filkorn [63] [81]
37Michael J. Foster [25] [28]
38Nissim Francez [16] [21]
39Masahiro Fujita [60] [68] [78] [93] [118] [120] [133] [143] [163] [221]
40Steven M. German [15] [17] [19] [31] [40] [89] [113] [132]
41Enrico Giunchiglia [148]
42Fausto Giunchiglia [107] [123] [125] [126] [148]
43David P. Gluch [163]
44Amit Goel [131]
45Alex Groce [160] [165] [169] [170] [172] [179]
46Orna Grumberg [30] [33] [34] [35] [36] [41] [42] [52] [55] [59] [62] [66] [70] [74] [79] [80] [84] [95] [96] [111] [127] [134] [139] [151] [159] [166] [190] [217] [223]
47Anubhav Gupta [135] [149] [168] [187] [191]
48Yuri Gurevich [16]
49Joseph Y. Halpern [15] [17] [19] [31] [40]
50Kiyoharu Hamaguchi [70] [95]
51Zhi Han [152] [157]
52Leonard A. Harris [216]
53Vasilili Hartonas-Garmhausen [116]
54Vassili Hartonas-Garmhausen [88] [99]
55Vicky Hartonas-Garmhausen [107] [124] [125]
56Hiromi Hiraishi [62] [69] [74]
57Pei-Hsin Ho [86]
58Yatin Vasant Hoskote [86]
59L. J. Hwang [45] [54]
60Himanshu Jain [175] [187] [188] [195] [199] [203] [204] [209] [217] [223] [228]
61Jawahar Jain [133]
62Somesh Jha [62] [63] [71] [74] [75] [80] [81] [91] [96] [98] [106] [110] [121] [128] [129] [130] [134] [139] [140] [141] [142] [146] [150] [151] [160] [169] [184]
63Sumit Kumar Jha [186] [192] [207] [216] [229]
64Timothy Kam [86]
65Jorge Kanda [172]
66James Kapinski [215]
67Manpreet Khaira [86] [87]
68Nicholas Kidd [198]
69Dexter Kozen [22]
70Daniel Kroening (Daniel Kröning) [162] [164] [171] [173] [174] [175] [178] [179] [180] [181] [183] [189] [195] [203] [204] [209]
71Bruce H. Krogh [152] [157] [192] [207] [215]
72Andreas Kuehlmann [114]
73James H. Kukula [141] [142] [147] [149]
74Robert P. Kurshan [42] [48] [51] [52] [57]
75Marta Z. Kwiatkowska [99]
76Christopher James Langmead [216] [229]
77Axel Legay [214] [216] [229]
78Flavio Lerda [174] [202] [215]
79Lishing Liu [5]
80David E. Long [43] [44] [49] [50] [53] [55] [59] [62] [65] [66] [71] [74] [84] [91]
81Yuan Lu [98] [121] [132] [133] [134] [139] [146] [151]
82Stephen Magill [205]
83Wilfredo R. Marrero [69] [71] [76] [77] [91] [106] [128] [129] [150]
84Will Marrero [130]
85Anmol Mathur [221]
86Patrick C. McGeer [68]
87Kenneth L. McMillan [44] [45] [46] [54] [60] [62] [65] [74] [79] [88] [93]
88Vaibhav Mehta [200]
89Albert R. Meyer [21]
90Spiro Michaylov [39] [43] [53]
91Marius Minea [69] [76] [77] [92] [98] [102] [111] [114] [201]
92Bhubaneswaru Mishra [23]
93Bud Mishra (Bhubaneswar Mishra) [20] [25] [26] [28]
94C. Robert Morgan [10]
95Edjard Mota [172]
96Linda A. Ness [62] [74]
97Christos Nikolaou [13]
98John W. O'Leary [86]
99Waleska Oliveira [172]
100Joël Ouaknine [152] [153] [170] [173] [176] [177] [183] [185] [190]
101Doron Peled [111]
102Marco Pistore [148]
103André Platzer [206] [218] [222] [227] [229]
104Richard Raimi [122] [137]
105Sreeranga P. Rajan [120] [143]
106Thomas W. Reps [120] [143] [198]
107Eric S. Roberts [10]
108Marco Roveri [123] [126] [148]
109Mark Ryan (Mark Dermot Ryan) [99]
110Samir Sapra [147] [161]
111Bernd-Holger Schlingloff [64] [138]
112Roberto Sebastiani [148]
113Subash Shankar [108] [120] [143]
114Natasha Sharygina [171] [176] [177] [185] [189] [190] [193] [194] [195] [204] [209] [210]
115Atsufumi Shibayama [64]
116Thomas R. Shiple [141]
117Joseph Sifakis [224]
118Nishant Sinha [177] [185] [188] [193] [194] [196] [208] [210]
119A. Prasad Sistla [14] [16] [18] [21] [24] [29] [110]
120Ofer Strichman [149] [154] [165] [168] [170] [173] [183]
121Olaf Stursberg [152] [157]
122Armando Tacchella [148]
123Muralidhar Talupur [158] [159] [166] [182] [197] [211]
124Tim Teitelbaum [120] [143]
125Marcio Teixeira [114]
126Prasanna Thati (Prasannaa Thati) [196]
127Michael Theobald [152] [157] [161]
128Ferucio Laurentiu Tiplea [201]
129Tayssir Touili [182] [190] [198]
130Yih-Kuen Tsay [212] [225]
131Pascal Urard [221]
132Helmut Veith [132] [134] [139] [140] [141] [142] [146] [147] [151] [155] [158] [160] [169] [182] [184] [186] [187] [190] [197] [211]
133Bow-Yaw Wang [212] [225]
134Dong Wang [121] [132] [141] [142] [147] [158] [159] [166]
135James E. Weimer [207]
136Poul Frederick Williams [135]
137Jeannette M. Wing [82] [83] [200]
138J. Yang [60] [93]
139Jerry Chih-Yuan Yang [68]
140Tomohiro Yoneda [64]
141Karen Yorav (Karen Laster) [153] [162] [164] [170] [171] [189]
142Xudong Zhao [56] [60] [68] [72] [78] [79] [85] [86] [87] [89] [90] [93] [104] [113]
143Haifeng Zhu [200]
144Yunshan Zhu [109] [115] [117] [118] [119] [122] [137] [144] [154]
145Paolo Zuliani [229]

Colors in the list of coauthors

Copyright © Fri Mar 12 12:56:28 2010 by Michael Ley (ley@uni-trier.de)