| |
 |      |
                                              |
Note: Links lead to the DBLP on the Web. Edmund M. Clarke Sagar Chaki , Edmund M. Clarke, Joël Ouaknine , Natasha Sharygina , Nishant Sinha : State/Event-Based Software Model Checking. IFM 2004 : 128-147 Edmund M. Clarke, Daniel Kroening , Flavio Lerda : A Tool for Checking ANSI-C Programs. TACAS 2004 : 168-176 Edmund M. Clarke, Daniel Kroening , Joël Ouaknine , Ofer Strichman : Completeness and Complexity of Bounded Model Checking. VMCAI 2004 : 85-96 Edmund M. Clarke: SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. CADE 2003 : 1 Edmund M. Clarke, Orna Grumberg , Muralidhar Talupur , Dong Wang : Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. CAV 2003 : 126-140 Sagar Chaki , Edmund M. Clarke, Alex Groce , Ofer Strichman : Predicate Abstraction with Minimum Predicates. CHARME 2003 : 19-34 Edmund M. Clarke, Daniel Kroening , Karen Yorav : Behavioral consistency of C and verilog programs using bounded model checking. DAC 2003 : 368-371 Edmund M. Clarke, Masahiro Fujita , David P. Gluch : Model Checking for Dependable Software-Intensive Systems. DSN 2003 : 764 Edmund M. Clarke, Daniel Kroening , Karen Yorav : Specifying and Verifying Systems with Multiple Clocks. ICCD 2003 : 48- Samir Sapra , Michael Theobald , Edmund M. Clarke: SAT-Based Algorithms for Logic Minimization. ICCD 2003 : 510- Sagar Chaki , Edmund M. Clarke, Alex Groce , Somesh Jha , Helmut Veith : Modular Verification of Software Components in C. ICSE 2003 : 385-395 Edmund M. Clarke, Orna Grumberg , Muralidhar Talupur , Dong Wang : High Level Verification of Control Intensive Systems Using Predicate Abstraction. MEMOCODE 2003 : 55-64 Edmund M. Clarke, Muralidhar Talupur , Helmut Veith , Dong Wang : SAT Based Predicate Abstraction for Hardware Verification. SAT 2003 : 78-92 Edmund M. Clarke, Ansgar Fehnker , Zhi Han , Bruce H. Krogh , Olaf Stursberg , Michael Theobald : Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. TACAS 2003 : 192-207 Edmund M. Clarke: Counterexample-Guided Abstraction Refinement. TIME 2003 : 7 Edmund M. Clarke, Helmut Veith : Counterexamples Revisited: Principles, Algorithms, Applications. Verification: Theory and Practice 2003 : 208-224 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) Edmund M. Clarke, Ansgar Fehnker , Zhi Han , Bruce H. Krogh , Joël Ouaknine , Olaf Stursberg , Michael Theobald : Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems. Int. J. Found. Comput. Sci. 14 (4): 583-604 (2003) Edmund M. Clarke, Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith : Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50 (5): 752-794 (2003) Edmund M. Clarke, Somesh Jha , Wilfredo R. Marrero : Efficient verification of security protocols using partial-order reductions. STTT 4 (2): 173-188 (2003) Edmund M. Clarke, Anubhav Gupta , James H. Kukula , Ofer Strichman : SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. CAV 2002 : 265-279 Alessandro Cimatti , Edmund M. Clarke, Enrico Giunchiglia , Fausto Giunchiglia , Marco Pistore , Marco Roveri , Roberto Sebastiani , Armando Tacchella : NuSMV 2: An OpenSource Tool for Symbolic Model Checking. CAV 2002 : 359-364 Pankaj Chauhan , Edmund M. Clarke, James H. Kukula , Samir Sapra , Helmut Veith , Dong Wang : Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis. FMCAD 2002 : 33-51 Edmund M. Clarke, Somesh Jha , Yuan Lu , Helmut Veith : Tree-Like Counterexamples in Model Checking. LICS 2002 : 19-29 Edmund M. Clarke: SAT-Based Counterexample Guided Abstraction Refinement. SPIN 2002 : 1 Sergey Berezin , Edmund M. Clarke, Armin Biere , Yunshan Zhu : Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function. Formal Methods in System Design 20 (2): 159-186 (2002) Edmund M. Clarke, Masahiro Fujita , Sreeranga P. Rajan , Thomas W. Reps , Subash Shankar , Tim Teitelbaum : Program slicing for VHDL. STTT 4 (1): 125-137 (2002) Pankay Chauhan , Edmund M. Clarke, Somesh Jha , James H. Kukula , Helmut Veith , Dong Wang : Using Combinatorial Optimization Methods for Quantification Scheduling. CHARME 2001 : 293-309 Pankaj Chauhan , Edmund M. Clarke, Somesh Jha , James H. Kukula , Thomas R. Shiple , Helmut Veith , Dong Wang : Non-linear Quantification Scheduling in Image Computation. ICCAD 2001 : 293- Alexis Campailla , Sagar Chaki , Edmund M. Clarke, Somesh Jha , Helmut Veith : Efficient Filtering in Publish-Subscribe Systems Using Binary Decision. ICSE 2001 : 443-452 Edmund M. Clarke, Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith : Progress on the State Explosion Problem in Model Checking. Informatics 2001 : 176-194 Edmund M. Clarke, Bernd-Holger Schlingloff : Model Checking. Handbook of Automated Reasoning 2001 : 1635-1790 Edmund M. Clarke, Armin Biere , Richard Raimi , Yunshan Zhu : Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design 19 (1): 7-34 (2001) Sérgio Vale Aguiar Campos , Edmund M. Clarke: The Verus language: representing time efficiently with BDDs. Theor. Comput. Sci. 253 (1): 95-118 (2001) Poul Frederick Williams , Armin Biere , Edmund M. Clarke, Anubhav Gupta : Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. CAV 2000 : 124-138 Edmund M. Clarke, Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith : Counterexample-Guided Abstraction Refinement. CAV 2000 : 154-169 Yuan Lu , Jawahar Jain , Edmund M. Clarke, Masahiro Fujita : Efficient variable ordering using aBDD based sampling. DAC 2000 : 687-692 Edmund M. Clarke, Steven M. German , Yuan Lu , Helmut Veith , Dong Wang : Executable Protocol Specification in ESL. FMCAD 2000 : 197-216 Randal E. Bryant , Pankay Chauhan , Edmund M. Clarke, Amit Goel : A Theory of Consistency for Modular Synchronous Systems. FMCAD 2000 : 486-504 Edmund M. Clarke, Somesh Jha , Wilfredo R. Marrero : Partial Order Reductions for Security Protocol Verification. TACAS 2000 : 503-518 Edmund M. Clarke, Somesh Jha , Wilfredo R. Marrero : Verifying security protocols with Brutus. ACM Trans. Softw. Eng. Methodol. 9 (4): 443-487 (2000) 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) Alessandro Cimatti , Edmund M. Clarke, Fausto Giunchiglia , Marco Roveri : NUSMV: A New Symbolic Model Checker. STTT 2 (4): 410-425 (2000) Vicky Hartonas-Garmhausen , Sérgio Vale Aguiar Campos , Alessandro Cimatti , Edmund M. Clarke, Fausto Giunchiglia : Verification of a safety-critical railway interlocking system with real-time constraints. Sci. Comput. Program. 36 (1): 53-64 (2000) Vicky Hartonas-Garmhausen , Sérgio Vale Aguiar Campos , Edmund M. Clarke: ProbVerus: Probabilistic Symbolic Model Checking. ARTS 1999 : 96-110 Alessandro Cimatti , Edmund M. Clarke, Fausto Giunchiglia , Marco Roveri : NUSMV: A New Symbolic Model Verifier. CAV 1999 : 495-499 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 Edmund M. Clarke, Somesh Jha , Yuan Lu , Dong Wang : Abstract BDDs: A Technque for Using Abstraction in Model Checking. CHARME 1999 : 172-186 Edmund M. Clarke, Masahiro Fujita , Sreeranga P. Rajan , Thomas W. Reps , Subash Shankar , Tim Teitelbaum : Program Slicing of Hardware Description Languages. CHARME 1999 : 298-312 Armin Biere , Edmund M. Clarke, Yunshan Zhu : Multiple State and Single State Tableaux for Combining Local and Global Model Checking. Correct System Design 1999 : 163-179 Armin Biere , Alessandro Cimatti , Edmund M. Clarke, Masahiro Fujita , Yunshan Zhu : Symbolic Model Checking Using SAT Procedures instead of BDDs. DAC 1999 : 317-320 Armin Biere , Alessandro Cimatti , Edmund M. Clarke, Yunshan Zhu : Symbolic Model Checking without BDDs. TACAS 1999 : 193-207 Christel Baier , Edmund M. Clarke, Vasiliki Hartonas-Garmhausen : On the Semantic Foundations of Probabilistic Synchronous Reactive Programs. Electr. Notes Theor. Comput. Sci. 22 : (1999) Armin Biere , Edmund M. Clarke, Yunshan Zhu : Combining Local and Global Model Checking. Electr. Notes Theor. Comput. Sci. 23 (2): (1999) Sérgio Vale Aguiar Campos , Marcio Teixeira , Marius Minea , Andreas Kuehlmann , Edmund M. Clarke: Model Checking Semi-Continuous Time Models Using BDDs. Electr. Notes Theor. Comput. Sci. 23 (2): (1999) Edmund M. Clarke, Steven M. German , Xudong Zhao : Verifying the SRT Division Algorithm Using Theorem Proving Techniques. Formal Methods in System Design 14 (1): 7-44 (1999) Sérgio Vale Aguiar Campos , Edmund M. Clarke: Analysis and Verification of Real-Time Systems Using Quantitative Symbolic Algorithms. STTT 2 (3): 260-269 (1999) Edmund M. Clarke, Orna Grumberg , Marius Minea , Doron Peled : State Space Reduction Using Partial Order Techniques. STTT 2 (3): 279-287 (1999) Edmund M. Clarke, E. Allen Emerson , Somesh Jha , A. Prasad Sistla : Symmetry Reductions inModel Checking. CAV 1998 : 147-158 Sergey Berezin , Armin Biere , Edmund M. Clarke, Yunshan Zhu : Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. FMCAD 1998 : 369-386 David Déharbe , Subash Shankar , Edmund M. Clarke: Model Checking VHDL with CV. FMCAD 1998 : 508-514 Vicky Hartonas-Garmhausen , Sérgio Vale Aguiar Campos , Alessandro Cimatti , Edmund M. Clarke, Fausto Giunchiglia : Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints. FTCS 1998 : 458-463 Edmund M. Clarke, Somesh Jha , Wilfredo R. Marrero : Using state space exploration and a natural deduction style message derivation engine to verify security protocols. PROCOMET 1998 : 87-106 Edmund M. Clarke, Sergey Berezin : Model Checking: Historical Perspective and Example (Extended Abstract). TABLEAUX 1998 : 18-24 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) Sérgio Vale Aguiar Campos , Edmund M. Clarke: The Versus Language: Representing Time Efficiently with BDDs. ARTS 1997 : 64-78 Sérgio Vale Aguiar Campos , Edmund M. Clarke, Marius Minea : The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems. CAV 1997 : 452-455 Sergey Berezin , Sérgio Vale Aguiar Campos , Edmund M. Clarke: Compositional Reasoning in Model Checking. COMPOS 1997 : 81-102 Edmund M. Clarke: Model Cheking. FSTTCS 1997 : 54-56 Christel Baier , Edmund M. Clarke, Vassili Hartonas-Garmhausen , Marta Z. Kwiatkowska , Mark Ryan : Symbolic Model Checking for Probabilistic Processes. ICALP 1997 : 430-440 Somesh Jha , Y. Lu , Marius Minea , Edmund M. Clarke: Equivalence Checking Using AbstractBDDs. ICCD 1997 : 332-337 Edmund M. Clarke: Temporal Logic Model Checking (Abstract). ILPS 1997 : 3 Edmund M. Clarke, Orna Grumberg , Somesh Jha : Verifying Parameterized Networks. ACM Trans. Program. Lang. Syst. 19 (5): 726-750 (1997) Edmund M. Clarke, Orna Grumberg , Kiyoharu Hamaguchi : Another Look at LTL Model Checking. Formal Methods in System Design 10 (1): 47-71 (1997) Edmund M. Clarke: Editorial. Formal Methods in System Design 10 (1): 5 (1997) Edmund M. Clarke, Kenneth L. McMillan , X. Zhao , Masahiro Fujita , J. Yang : Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. Formal Methods in System Design 10 (2/3): 137-148 (1997) Sérgio Vale Aguiar Campos , Edmund M. Clarke, Marius Minea : Symbolic Techniques for Formally Verifying Industrial Systems. Sci. Comput. Program. 29 (1-2): 79-98 (1997) Anca Browne , Edmund M. Clarke, Somesh Jha , David E. Long , Wilfredo R. Marrero : An Improved Algorithm for the Evaluation of Fixpoint Expressions. Theor. Comput. Sci. 178 (1-2): 237-255 (1997) Andrej Bauer , Edmund M. Clarke, Xudong Zhao : Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation. AISMC 1996 : 21-37 Edmund M. Clarke, Steven M. German , Xudong Zhao : Verifying the SRT Division Algorithm Using Theorem Proving Techniques. CAV 1996 : 111-122 Edmund M. Clarke, Kenneth L. McMillan , Sérgio Vale Aguiar Campos , Vassili Hartonas-Garmhausen : Symbolic Model Checking. CAV 1996 : 419-427 Edmund M. Clarke, Manpreet Khaira , Xudong Zhao : Word Level Model Checking - Avoiding the Pentium FDIV Error. DAC 1996 : 645-648 Yirng-An Chen , Edmund M. Clarke, Pei-Hsin Ho , Yatin Vasant Hoskote , Timothy Kam , Manpreet Khaira , John W. O'Leary , Xudong Zhao : Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking. FMCAD 1996 : 19-33 Edmund M. Clarke, Xudong Zhao : Word Level Model Checking (Abstract). MFCS 1996 : 1 Edmund M. Clarke, Jeannette M. Wing : Formal Methods: State of the Art and Future Directions. ACM Comput. Surv. 28 (4): 626-643 (1996) Edmund M. Clarke, Jeannette M. Wing : Tools and Partial Analysis. ACM Comput. Surv. 28 (4es): 116 (1996) Edmund M. Clarke, Somesh Jha , Reinhard Enders , Thomas Filkorn : Exploiting Symmetry in Temporal Logic Model Checking. Formal Methods in System Design 9 (1/2): 77-104 (1996) Edmund M. Clarke, Orna Grumberg , Somesh Jha : Veryfying Parameterized Networks using Abstraction and Regular Languages. CONCUR 1995 : 395-407 Edmund M. Clarke, Orna Grumberg , Kenneth L. McMillan , X. Zhao : Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. DAC 1995 : 427-432 Sérgio Vale Aguiar Campos , Edmund M. Clarke, Wilfredo R. Marrero , Marius Minea : Verifying the performance of the PCI local bus using symbolic techniques. ICCD 1995 : 72-78 Sérgio Vale Aguiar Campos , Edmund M. Clarke, Wilfredo R. Marrero , Marius Minea : Verus: A Tool for Quantitative Analysis of Finite-State Real-Time Systems. Workshop on Languages, Compilers, & Tools for Real-Time Systems 1995 : 70-78 Edmund M. Clarke, Somesh Jha : Symmetry and Induction in Model Checking. Computer Science Today 1995 : 455-470 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) Edmund M. Clarke: Automatic Verification of Finite-state Concurrent Systems. Application and Theory of Petri Nets 1994 : 1 Edmund M. Clarke, Xudong Zhao : Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan. CADE 1994 : 758-763 David E. Long , Anca Browne , Edmund M. Clarke, Somesh Jha , Wilfredo R. Marrero : An Improved Algorithm for the Evaluation of Fixpoint Expressions. CAV 1994 : 338-350 Edmund M. Clarke, Orna Grumberg , Kiyoharu Hamaguchi : Another Look at LTL Model Checking. CAV 1994 : 415-427 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 Masahiro Fujita , Jerry Chih-Yuan Yang , Edmund M. Clarke, Xudong Zhao , Patrick C. McGeer : Fast Spectrum Computation for Logic Functions using Binary Decision Diagrams. ISCAS 1994 : 275-278 Edmund M. Clarke: Automatic Verification of Finite-State Concurrent Systems LICS 1994 : 126 Edmund M. Clarke, Orna Grumberg , David E. Long : Model Checking and Abstraction. ACM Trans. Program. Lang. Syst. 16 (5): 1512-1542 (1994) Tomohiro Yoneda , Atsufumi Shibayama , Bernd-Holger Schlingloff , Edmund M. Clarke: Efficient Verification of Parallel Real-Time Systems. CAV 1993 : 321-346 Edmund M. Clarke, Thomas Filkorn , Somesh Jha : Exploiting Symmetry In Temporal Logic Model Checking. CAV 1993 : 450-462 Edmund M. Clarke, Orna Grumberg , Hiromi Hiraishi , Somesh Jha , David E. Long , Kenneth L. McMillan , Linda A. Ness : Verification of the Futurebus+ Cache Coherence Protocol. CHDL 1993 : 15-30 Edmund M. Clarke: Automatic Verification of Sequential Circuit Designs. CHDL 1993 : 165 Edmund M. Clarke, Kenneth L. McMillan , Xudong Zhao , Masahiro Fujita , J. Yang : Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. DAC 1993 : 54-60 Edmund M. Clarke, Orna Grumberg , David E. Long : Verification Tools for Finite-State Concurrent Systems. REX School/Symposium 1993 : 124-175 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) Edmund M. Clarke, Xudong Zhao : Analytica - A Theorem Prover in Mathematica. CADE 1992 : 761-765 Edmund M. Clarke, Orna Grumberg , David E. Long : Model Checking and Abstraction. POPL 1992 : 342-354 Jerry R. Burch , Edmund M. Clarke, Kenneth L. McMillan , David L. Dill , L. J. Hwang : Symbolic Model Checking: 10^20 States and Beyond Inf. Comput. 98 (2): 142-170 (1992) Soumitra Bose , Edmund M. Clarke, David E. Long , Spiro Michaylov : PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. J. Autom. Reasoning 8 (2): 153-181 (1992) Edmund M. Clarke, Orna Grumberg , Robert P. Kurshan : A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. J. Log. Comput. 2 (5): 605-618 (1992) Edmund M. Clarke, Robert P. Kurshan : Computer Aided Verification, 2nd International Workshop, CAV '90, New Brunswick, NJ, USA, June 18-21, 1990, Proceedings Springer 1991 Jerry R. Burch , Edmund M. Clarke, David E. Long : Representing Circuits More Efficiently in Symbolic Model Checking. DAC 1991 : 403-407 Jerry R. Burch , Edmund M. Clarke, David E. Long : Symbolic Model Checking with Partitioned Transistion Relations. VLSI 1991 : 49-58 Edmund M. Clarke, I. A. Browne , Robert P. Kurshan : A Unified Approach For Showing Language Containment And Equivalence Between Various Types Of Omega-Automata. CAAP 1990 : 103-116 Edmund M. Clarke: Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem. CAV 1990 : 1 Jerry R. Burch , Edmund M. Clarke, Kenneth L. McMillan , David L. Dill : Sequential Circuit Verification Using Symbolic Model Checking. DAC 1990 : 46-51 Jerry R. Burch , Edmund M. Clarke, Kenneth L. McMillan , David L. Dill , L. J. Hwang : Symbolic Model Checking: 10^20 States and Beyond LICS 1990 : 428-439 Edmund M. Clarke, David E. Long , Kenneth L. McMillan : Compositional Model Checking LICS 1989 : 353-362 Soumitra Bose , Edmund M. Clarke, David E. Long , Spiro Michaylov : PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses LICS 1989 : 80-89 Edmund M. Clarke, Orna Grumberg , Robert P. Kurshan : A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. Logic at Botik 1989 : 81-90 Michael C. Browne , Edmund M. Clarke, Orna Grumberg : Reasoning about Networks with Many Identical Finite State Processes Inf. Comput. 81 (1): 13-31 (1989) Steven M. German , Edmund M. Clarke, Joseph Y. Halpern : Reasoning about Procedures as Parameters in the Language L4 Inf. Comput. 83 (3): 265-359 (1989) P. E. Allen , Soumitra Bose , Edmund M. Clarke, Spiro Michaylov : PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. CADE 1988 : 764-765 Edmund M. Clarke, I. A. Draghicescu : Expressibility results for linear-time and branching-time logics. REX Workshop 1988 : 428-437 Michael C. Browne , Edmund M. Clarke, Orna Grumberg : Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theor. Comput. Sci. 59 : 115-131 (1988) Edmund M. Clarke, Orna Grumberg : Avoiding The State Explosion Problem in Temporal Logic Model Checking. PODC 1987 : 294-303 Michael C. Browne , Edmund M. Clarke, Orna Grumberg : Characterizing Kripke Structures in Temporal Logic. TAPSOFT, Vol.1 1987 : 256-270 Edmund M. Clarke, Orna Grumberg : The Model Checking Problem for Concurrent Systems with Many Similar Processes. Temporal Logic in Specification 1987 : 188-201 Edmund M. Clarke, Yulin Feng : Escher - a geometrical layout system for recursively defined circuits. DAC 1986 : 650-653 Steven M. German , Edmund M. Clarke, Joseph Y. Halpern : True Relative Completeness of an Axiom System for the Language L4 (Abridged) LICS 1986 : 11-25 Edmund M. Clarke, Orna Grumberg , Michael C. Browne : Reasoning About Networks With Many Identical Finite-State Processes. PODC 1986 : 240-248 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) Thomas S. Anantharaman , Edmund M. Clarke, Michael J. Foster , B. Mishra : Compiling Path Expressions Into VLSI Circuits. Distributed Computing 1 (3): 150-166 (1986) Edmund M. Clarke: Distributed Computing Issues in Hardware Design. Distributed Computing 1 (4): 185-186 (1986) Michael C. Browne , Edmund M. Clarke, David L. Dill , Bud Mishra : Automatic Verification of Sequential Circuits Using Temporal Logic. IEEE Trans. Computers 35 (12): 1035-1044 (1986) Thomas S. Anantharaman , Edmund M. Clarke, M. J. Foster , B. Mishra : Compiling Path Expressions into VLSI Circuits. POPL 1985 : 191-204 A. Prasad Sistla , Edmund M. Clarke: The Complexity of Propositional Linear Temporal Logics J. ACM 32 (3): 733-749 (1985) B. Mishra , Edmund M. Clarke: Hierarchical Verification of Asynchronous Circuits Using Temporal Logic. Theor. Comput. Sci. 38 : 269-291 (1985) Edmund M. Clarke, Dexter Kozen : Logic of Programs, Workshop, Carnegie Mellon University, Pittsburgh, PA, USA, June 6-8, 1983, Proceedings Springer 1984 A. Prasad Sistla , Edmund M. Clarke, Nissim Francez , Albert R. Meyer : Can Message Buffers Be Axiomatized in Linear Temporal Logic? Information and Control 63 (1/2): 88-112 (1984) Edmund M. Clarke, Bud Mishra : Automatic Verification of Asynchronous Circuits. Logic of Programs 1983 : 101-115 Steven M. German , Edmund M. Clarke, Joseph Y. Halpern : Reasoning About Procedures as Parameters. Logic of Programs 1983 : 206-220 Edmund M. Clarke, E. Allen Emerson , A. Prasad Sistla : Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. POPL 1983 : 117-126 Edmund M. Clarke, Steven M. German , Joseph Y. Halpern : Effective Axiomatizations of Hoare Logics J. ACM 30 (3): 612-636 (1983) A. Prasad Sistla , Edmund M. Clarke, Nissim Francez , Yuri Gurevich : Can Message Buffers be Characterized in Linear Temporal Logic? PODC 1982 : 148-156 Edmund M. Clarke, Steven M. German , Joseph Y. Halpern : On Effective Axiomatizations of Hoare Logics. POPL 1982 : 309-321 A. Prasad Sistla , Edmund M. Clarke: The Complexity of Propositional Linear Temporal Logics STOC 1982 : 159-168 Edmund M. Clarke, Christos Nikolaou : Distributed Reconfiguration Strategies for Fault-Tolerant Multiprocessor Systems. IEEE Trans. Computers 31 (8): 771-784 (1982) E. Allen Emerson , Edmund M. Clarke: Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. Sci. Comput. Program. 2 (3): 241-266 (1982) Edmund M. Clarke, E. Allen Emerson : Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logic of Programs 1981 : 52-71 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) E. Allen Emerson , Edmund M. Clarke: Characterizing Correctness Properties of Parallel Programs Using Fixpoints. ICALP 1980 : 169-181 Philip A. Bernstein , Barbara T. Blaustein , Edmund M. Clarke: Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data. VLDB 1980 : 126-136 Edmund M. Clarke: Synthesis of Resource Invariants for Concurrent Programs. ACM Trans. Program. Lang. Syst. 2 (3): 338-358 (1980) Edmund M. Clarke: Proving Correctness of Coroutines Without History Variables. Acta Inf. 13 : 169-188 (1980) Edmund M. Clarke, Lishing Liu : Approximate Algorithms for Optimization of Busy Waiting in Parallel Programs (Preliminary Report) FOCS 1979 : 255-266 Edmund M. Clarke: Synthesis of Resource Invariants for Concurrent Programs. POPL 1979 : 211-221 Edmund M. Clarke: Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems. J. ACM 26 (1): 129-147 (1979) Edmund M. Clarke: Program Invariants as Fixed Points (Preliminary Reports) FOCS 1977 : 18-29 Edmund M. Clarke: Programming Language Constructs for Which it is Impossible to Obtain ``Good'' Hoare-Like Axiom Systems. POPL 1977 : 10-20 1 [ 38 ] 2 [ 25 ] [ 28 ] 3 [ 94 ] [ 111 ] 4 [ 85 ] [ 99 ] 5 [ 96 ] [ 100 ] [ 104 ] [ 138 ] 6 [ 8 ] 7 [ 104 ] [ 110 ] [ 112 ] [ 113 ] [ 114 ] [ 117 ] [ 129 ] [ 131 ] [ 138 ] 8 [ 8 ] 9 [ 38 ] [ 42 ] [ 52 ] 10 [ 68 ] [ 86 ] 11 [ 47 ] 12 [ 26 ] [ 30 ] [ 34 ] [ 36 ] [ 40 ] 13 [ 125 ] 14 [ 44 ] [ 45 ] [ 48 ] [ 49 ] [ 53 ] 15 [ 134 ] 16 [ 66 ] [ 73 ] [ 74 ] [ 83 ] [ 87 ] [ 96 ] [ 97 ] [ 98 ] [ 102 ] [ 107 ] [ 109 ] [ 119 ] [ 120 ] [ 122 ] [ 130 ] 17 [ 134 ] [ 147 ] [ 153 ] [ 158 ] [ 163 ] 18 [ 135 ] [ 141 ] 19 [ 125 ] [ 136 ] 20 [ 81 ] 21 [ 102 ] [ 112 ] [ 113 ] [ 118 ] [ 120 ] [ 121 ] [ 142 ] 22 [ 103 ] 23 [ 26 ] [ 44 ] [ 45 ] [ 53 ] 24 [ 37 ] [ 56 ] 25 [ 9 ] [ 11 ] [ 12 ] [ 18 ] [ 29 ] [ 105 ] 26 [ 77 ] 27 [ 10 ] 28 [ 146 ] [ 150 ] 29 [ 32 ] 30 [ 61 ] [ 77 ] 31 [ 25 ] 32 [ 28 ] 33 [ 16 ] [ 21 ] 34 [ 58 ] [ 65 ] [ 88 ] [ 113 ] [ 115 ] [ 127 ] [ 137 ] [ 156 ] 35 [ 15 ] [ 17 ] [ 19 ] [ 31 ] [ 39 ] [ 84 ] [ 108 ] [ 126 ] 36 [ 142 ] 37 [ 102 ] [ 118 ] [ 120 ] [ 121 ] [ 142 ] 38 [ 156 ] 39 [ 125 ] 40 [ 153 ] [ 158 ] 41 [ 30 ] [ 33 ] [ 34 ] [ 35 ] [ 36 ] [ 40 ] [ 41 ] [ 51 ] [ 54 ] [ 57 ] [ 60 ] [ 63 ] [ 67 ] [ 71 ] [ 75 ] [ 76 ] [ 90 ] [ 91 ] [ 106 ] [ 122 ] [ 128 ] [ 133 ] [ 145 ] [ 152 ] [ 159 ] 42 [ 129 ] [ 143 ] 43 [ 16 ] 44 [ 15 ] [ 17 ] [ 19 ] [ 31 ] [ 39 ] 45 [ 67 ] [ 90 ] 46 [ 146 ] [ 150 ] 47 [ 111 ] 48 [ 83 ] [ 94 ] 49 [ 102 ] [ 119 ] [ 120 ] 50 [ 60 ] [ 66 ] [ 71 ] 51 [ 81 ] 52 [ 81 ] 53 [ 44 ] [ 53 ] 54 [ 127 ] 55 [ 60 ] [ 61 ] [ 68 ] [ 71 ] [ 72 ] [ 76 ] [ 77 ] [ 86 ] [ 91 ] [ 93 ] [ 101 ] [ 105 ] [ 116 ] [ 123 ] [ 124 ] [ 128 ] [ 133 ] [ 134 ] [ 135 ] [ 136 ] [ 140 ] [ 144 ] [ 145 ] [ 153 ] 56 [ 81 ] 57 [ 81 ] [ 82 ] 58 [ 22 ] 59 [ 155 ] [ 157 ] [ 161 ] [ 162 ] 60 [ 146 ] [ 150 ] 61 [ 109 ] 62 [ 135 ] [ 136 ] [ 141 ] [ 143 ] 63 [ 41 ] [ 47 ] [ 50 ] [ 51 ] [ 56 ] 64 [ 94 ] 65 [ 162 ] 66 [ 5 ] 67 [ 42 ] [ 43 ] [ 48 ] [ 49 ] [ 52 ] [ 54 ] [ 57 ] [ 60 ] [ 63 ] [ 68 ] [ 71 ] [ 86 ] 68 [ 93 ] 69 [ 116 ] [ 126 ] [ 127 ] [ 128 ] [ 133 ] [ 140 ] [ 145 ] 70 [ 66 ] [ 68 ] [ 73 ] [ 74 ] [ 86 ] [ 101 ] [ 123 ] [ 124 ] [ 144 ] 71 [ 65 ] 72 [ 43 ] [ 44 ] [ 45 ] [ 53 ] [ 58 ] [ 60 ] [ 71 ] [ 75 ] [ 83 ] [ 88 ] 73 [ 21 ] 74 [ 38 ] [ 42 ] [ 52 ] 75 [ 66 ] [ 73 ] [ 74 ] [ 87 ] [ 93 ] [ 97 ] [ 106 ] [ 109 ] 76 [ 23 ] [ 25 ] [ 28 ] 77 [ 20 ] [ 26 ] 78 [ 10 ] 79 [ 60 ] [ 71 ] 80 [ 13 ] 81 [ 81 ] 82 [ 146 ] [ 147 ] [ 161 ] [ 163 ] 83 [ 106 ] 84 [ 142 ] 85 [ 117 ] [ 131 ] 86 [ 115 ] [ 137 ] 87 [ 115 ] [ 137 ] 88 [ 10 ] 89 [ 118 ] [ 121 ] [ 142 ] 90 [ 94 ] 91 [ 141 ] [ 154 ] 92 [ 62 ] [ 132 ] 93 [ 142 ] 94 [ 103 ] [ 115 ] [ 137 ] 95 [ 163 ] 96 [ 62 ] 97 [ 135 ] 98 [ 163 ] 99 [ 14 ] [ 16 ] [ 18 ] [ 21 ] [ 24 ] [ 29 ] [ 105 ] 100 [ 143 ] [ 158 ] [ 161 ] 101 [ 146 ] [ 150 ] 102 [ 142 ] 103 [ 151 ] [ 152 ] [ 159 ] 104 [ 115 ] [ 137 ] 105 [ 109 ] 106 [ 146 ] [ 150 ] [ 154 ] 107 [ 126 ] [ 128 ] [ 133 ] [ 134 ] [ 135 ] [ 136 ] [ 140 ] [ 141 ] [ 145 ] [ 148 ] [ 151 ] [ 153 ] 108 [ 116 ] [ 126 ] [ 135 ] [ 136 ] [ 141 ] [ 151 ] [ 152 ] [ 159 ] 109 [ 129 ] 110 [ 78 ] [ 79 ] 111 [ 58 ] [ 88 ] 112 [ 65 ] 113 [ 62 ] 114 [ 147 ] [ 155 ] [ 157 ] 115 [ 75 ] [ 88 ] 116 [ 55 ] [ 58 ] [ 65 ] [ 69 ] [ 80 ] [ 81 ] [ 82 ] [ 84 ] [ 85 ] [ 99 ] [ 108 ] 117 [ 104 ] [ 110 ] [ 112 ] [ 113 ] [ 114 ] [ 117 ] [ 131 ] [ 138 ]  ©2004 Association for Computing Machinery |
