Search the dblp DataBase
Edmund M. Clarke :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
Philip A. Bernstein , Barbara T. Blaustein , Edmund M. Clarke Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data. [Citation Graph (32, 6)][DBLP ] VLDB, 1980, pp:126-136 [Conf ] Edmund M. Clarke , E. Allen Emerson , A. Prasad Sistla Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. [Citation Graph (7, 0)][DBLP ] ACM Trans. Program. Lang. Syst., 1986, v:8, n:2, pp:244-263 [Journal ] A. Prasad Sistla , Edmund M. Clarke The Complexity of Propositional Linear Temporal Logics [Citation Graph (5, 0)][DBLP ] J. ACM, 1985, v:32, n:3, pp:733-749 [Journal ] Edmund M. Clarke Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems. [Citation Graph (2, 0)][DBLP ] J. ACM, 1979, v:26, n:1, pp:129-147 [Journal ] E. Allen Emerson , Edmund M. Clarke Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons. [Citation Graph (2, 0)][DBLP ] Sci. Comput. Program., 1982, v:2, n:3, pp:241-266 [Journal ] Edmund M. Clarke , Orna Grumberg Avoiding The State Explosion Problem in Temporal Logic Model Checking. [Citation Graph (1, 0)][DBLP ] PODC, 1987, pp:294-303 [Conf ] Thomas S. Anantharaman , Edmund M. Clarke , Michael J. Foster , Bud Mishra Compiling Path Expressions into VLSI Circuits. [Citation Graph (1, 0)][DBLP ] POPL, 1985, pp:191-204 [Conf ] Jerry R. Burch , Edmund M. Clarke , Kenneth L. McMillan , David L. Dill , L. J. Hwang Symbolic Model Checking: 10^20 States and Beyond [Citation Graph (1, 0)][DBLP ] Inf. Comput., 1992, v:98, n:2, pp:142-170 [Journal ] Andrej Bauer , Edmund M. Clarke , Xudong Zhao Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation. [Citation Graph (0, 0)][DBLP ] AISMC, 1996, pp:21-37 [Conf ] Edmund M. Clarke Automatic Verification of Finite-state Concurrent Systems. [Citation Graph (0, 0)][DBLP ] Application and Theory of Petri Nets, 1994, pp:1- [Conf ] Sérgio Vale Aguiar Campos , Edmund M. Clarke The Verus Language: Representing Time Efficiently with BDDs. [Citation Graph (0, 0)][DBLP ] ARTS, 1997, pp:64-78 [Conf ] Vicky Hartonas-Garmhausen , Sérgio Vale Aguiar Campos , Edmund M. Clarke ProbVerus: Probabilistic Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] ARTS, 1999, pp:96-110 [Conf ] Armin Biere , Edmund M. Clarke , Yunshan Zhu Multiple State and Single State Tableaux for Combining Local and Global Model Checking. [Citation Graph (0, 0)][DBLP ] Correct System Design, 1999, pp:163-179 [Conf ] Edmund M. Clarke , Helmut Veith Counterexamples Revisited: Principles, Algorithms, Applications. [Citation Graph (0, 0)][DBLP ] Verification: Theory and Practice, 2003, pp:208-224 [Conf ] Edmund M. Clarke , Anca Browne , Robert P. Kurshan A Unified Approach For Showing Language Containment And Equivalence Between Various Types Of Omega-Automata. [Citation Graph (0, 0)][DBLP ] CAAP, 1990, pp:103-116 [Conf ] P. E. Allen , Soumitra Bose , Edmund M. Clarke , Spiro Michaylov PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. [Citation Graph (0, 0)][DBLP ] CADE, 1988, pp:764-765 [Conf ] Edmund M. Clarke , Xudong Zhao Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan. [Citation Graph (0, 0)][DBLP ] CADE, 1994, pp:758-763 [Conf ] Edmund M. Clarke , Xudong Zhao Analytica - A Theorem Prover in Mathematica. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:761-765 [Conf ] Edmund M. Clarke SAT-Based Counterexample Guided Abstraction Refinement in Model Checking. [Citation Graph (0, 0)][DBLP ] CADE, 2003, pp:1- [Conf ] Armin Biere , Edmund M. Clarke , Richard Raimi , Yunshan Zhu Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs. [Citation Graph (0, 0)][DBLP ] CAV, 1999, pp:60-71 [Conf ] Sérgio Vale Aguiar Campos , Edmund M. Clarke , Marius Minea The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems. [Citation Graph (0, 0)][DBLP ] CAV, 1997, pp:452-455 [Conf ] Sagar Chaki , Edmund M. Clarke , Nishant Sinha , Prasanna Thati Automated Assume-Guarantee Reasoning for Simulation Conformance. [Citation Graph (0, 0)][DBLP ] CAV, 2005, pp:534-547 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] CAV, 2002, pp:359-364 [Conf ] Alessandro Cimatti , Edmund M. Clarke , Fausto Giunchiglia , Marco Roveri NUSMV: A New Symbolic Model Verifier. [Citation Graph (0, 0)][DBLP ] CAV, 1999, pp:495-499 [Conf ] Edmund M. Clarke Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem. [Citation Graph (0, 0)][DBLP ] CAV, 1990, pp:1- [Conf ] Edmund M. Clarke , E. Allen Emerson , Somesh Jha , A. Prasad Sistla Symmetry Reductions inModel Checking. [Citation Graph (0, 0)][DBLP ] CAV, 1998, pp:147-158 [Conf ] Edmund M. Clarke , Thomas Filkorn , Somesh Jha Exploiting Symmetry In Temporal Logic Model Checking. [Citation Graph (0, 0)][DBLP ] CAV, 1993, pp:450-462 [Conf ] Edmund M. Clarke , Orna Grumberg , Kiyoharu Hamaguchi Another Look at LTL Model Checking. [Citation Graph (0, 0)][DBLP ] CAV, 1994, pp:415-427 [Conf ] Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith Counterexample-Guided Abstraction Refinement. [Citation Graph (0, 0)][DBLP ] CAV, 2000, pp:154-169 [Conf ] Edmund M. Clarke , Anubhav Gupta , James H. Kukula , Ofer Strichman SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques. [Citation Graph (0, 0)][DBLP ] CAV, 2002, pp:265-279 [Conf ] Edmund M. Clarke , Orna Grumberg , Muralidhar Talupur , Dong Wang Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates. [Citation Graph (0, 0)][DBLP ] CAV, 2003, pp:126-140 [Conf ] Edmund M. Clarke , Steven M. German , Xudong Zhao Verifying the SRT Division Algorithm Using Theorem Proving Techniques. [Citation Graph (0, 0)][DBLP ] CAV, 1996, pp:111-122 [Conf ] Edmund M. Clarke , Kenneth L. McMillan , Sérgio Vale Aguiar Campos , Vassili Hartonas-Garmhausen Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] CAV, 1996, pp:419-427 [Conf ] David E. Long , Anca Browne , Edmund M. Clarke , Somesh Jha , Wilfredo R. Marrero An Improved Algorithm for the Evaluation of Fixpoint Expressions. [Citation Graph (0, 0)][DBLP ] CAV, 1994, pp:338-350 [Conf ] Poul Frederick Williams , Armin Biere , Edmund M. Clarke , Anubhav Gupta Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] CAV, 2000, pp:124-138 [Conf ] Tomohiro Yoneda , Atsufumi Shibayama , Bernd-Holger Schlingloff , Edmund M. Clarke Efficient Verification of Parallel Real-Time Systems. [Citation Graph (0, 0)][DBLP ] CAV, 1993, pp:321-346 [Conf ] Sagar Chaki , Edmund M. Clarke , Alex Groce , Ofer Strichman Predicate Abstraction with Minimum Predicates. [Citation Graph (0, 0)][DBLP ] CHARME, 2003, pp:19-34 [Conf ] Pankaj Chauhan , Edmund M. Clarke , Somesh Jha , James H. Kukula , Helmut Veith , Dong Wang Using Combinatorial Optimization Methods for Quantification Scheduling. [Citation Graph (0, 0)][DBLP ] CHARME, 2001, pp:293-309 [Conf ] Edmund M. Clarke , Masahiro Fujita , Sreeranga P. Rajan , Thomas W. Reps , Subash Shankar , Tim Teitelbaum Program Slicing of Hardware Description Languages. [Citation Graph (0, 0)][DBLP ] CHARME, 1999, pp:298-312 [Conf ] Edmund M. Clarke , Somesh Jha , Yuan Lu , Dong Wang Abstract BDDs: A Technque for Using Abstraction in Model Checking. [Citation Graph (0, 0)][DBLP ] CHARME, 1999, pp:172-186 [Conf ] Edmund M. Clarke Automatic Verification of Sequential Circuit Designs. [Citation Graph (0, 0)][DBLP ] CHDL, 1993, pp:165- [Conf ] 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. [Citation Graph (0, 0)][DBLP ] CHDL, 1993, pp:15-30 [Conf ] Sergey Berezin , Sérgio Vale Aguiar Campos , Edmund M. Clarke Compositional Reasoning in Model Checking. [Citation Graph (0, 0)][DBLP ] COMPOS, 1997, pp:81-102 [Conf ] Edmund M. Clarke , Orna Grumberg , Somesh Jha Veryfying Parameterized Networks using Abstraction and Regular Languages. [Citation Graph (0, 0)][DBLP ] CONCUR, 1995, pp:395-407 [Conf ] Edmund M. Clarke , Muralidhar Talupur , Tayssir Touili , Helmut Veith Verification by Network Decomposition. [Citation Graph (0, 0)][DBLP ] CONCUR, 2004, pp:276-291 [Conf ] Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Masahiro Fujita , Yunshan Zhu Symbolic Model Checking Using SAT Procedures instead of BDDs. [Citation Graph (0, 0)][DBLP ] DAC, 1999, pp:317-320 [Conf ] Jerry R. Burch , Edmund M. Clarke , David E. Long Representing Circuits More Efficiently in Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] DAC, 1991, pp:403-407 [Conf ] Jerry R. Burch , Edmund M. Clarke , Kenneth L. McMillan , David L. Dill Sequential Circuit Verification Using Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] DAC, 1990, pp:46-51 [Conf ] Pankaj Chauhan , Edmund M. Clarke , Daniel Kroening A SAT-based algorithm for reparameterization in symbolic simulation. [Citation Graph (0, 0)][DBLP ] DAC, 2004, pp:524-529 [Conf ] Edmund M. Clarke , Yulin Feng Escher - a geometrical layout system for recursively defined circuits. [Citation Graph (0, 0)][DBLP ] DAC, 1986, pp:650-653 [Conf ] Edmund M. Clarke , Orna Grumberg , Kenneth L. McMillan , Xudong Zhao Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. [Citation Graph (0, 0)][DBLP ] DAC, 1995, pp:427-432 [Conf ] Edmund M. Clarke , Daniel Kroening , Karen Yorav Behavioral consistency of C and verilog programs using bounded model checking. [Citation Graph (0, 0)][DBLP ] DAC, 2003, pp:368-371 [Conf ] Edmund M. Clarke , Manpreet Khaira , Xudong Zhao Word Level Model Checking - Avoiding the Pentium FDIV Error. [Citation Graph (0, 0)][DBLP ] DAC, 1996, pp:645-648 [Conf ] Edmund M. Clarke , Kenneth L. McMillan , Xudong Zhao , Masahiro Fujita , J. Yang Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. [Citation Graph (0, 0)][DBLP ] DAC, 1993, pp:54-60 [Conf ] Himanshu Jain , Daniel Kroening , Natasha Sharygina , Edmund M. Clarke Word level predicate abstraction and refinement for verifying RTL verilog. [Citation Graph (0, 0)][DBLP ] DAC, 2005, pp:445-450 [Conf ] Yuan Lu , Jawahar Jain , Edmund M. Clarke , Masahiro Fujita Efficient variable ordering using aBDD based sampling. [Citation Graph (0, 0)][DBLP ] DAC, 2000, pp:687-692 [Conf ] Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith Progress on the State Explosion Problem in Model Checking. [Citation Graph (0, 0)][DBLP ] Informatics, 2001, pp:176-194 [Conf ] Edmund M. Clarke , Masahiro Fujita , David P. Gluch Model Checking for Dependable Software-Intensive Systems. [Citation Graph (0, 0)][DBLP ] DSN, 2003, pp:764- [Conf ] Edmund M. Clarke , Orna Grumberg , Robert P. Kurshan A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. [Citation Graph (0, 0)][DBLP ] Logic at Botik, 1989, pp:81-90 [Conf ] Natasha Sharygina , Sagar Chaki , Edmund M. Clarke , Nishant Sinha Dynamic Component Substitutability Analysis. [Citation Graph (0, 0)][DBLP ] FM, 2005, pp:512-528 [Conf ] Sergey Berezin , Armin Biere , Edmund M. Clarke , Yunshan Zhu Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. [Citation Graph (0, 0)][DBLP ] FMCAD, 1998, pp:369-386 [Conf ] Randal E. Bryant , Pankaj Chauhan , Edmund M. Clarke , Amit Goel A Theory of Consistency for Modular Synchronous Systems. [Citation Graph (0, 0)][DBLP ] FMCAD, 2000, pp:486-504 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] FMCAD, 2002, pp:33-51 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] FMCAD, 1996, pp:19-33 [Conf ] Edmund M. Clarke , Steven M. German , Yuan Lu , Helmut Veith , Dong Wang Executable Protocol Specification in ESL. [Citation Graph (0, 0)][DBLP ] FMCAD, 2000, pp:197-216 [Conf ] David Déharbe , Subash Shankar , Edmund M. Clarke Model Checking VHDL with CV. [Citation Graph (0, 0)][DBLP ] FMCAD, 1998, pp:508-514 [Conf ] Edmund M. Clarke , Natasha Sharygina , Nishant Sinha Program Compatibility Approaches. [Citation Graph (0, 0)][DBLP ] FMCO, 2005, pp:243-258 [Conf ] Edmund M. Clarke Program Invariants as Fixed Points (Preliminary Reports) [Citation Graph (0, 0)][DBLP ] FOCS, 1977, pp:18-29 [Conf ] Edmund M. Clarke , Lishing Liu Approximate Algorithms for Optimization of Busy Waiting in Parallel Programs (Preliminary Report) [Citation Graph (0, 0)][DBLP ] FOCS, 1979, pp:255-266 [Conf ] Edmund M. Clarke Model Cheking. [Citation Graph (0, 0)][DBLP ] FSTTCS, 1997, pp:54-56 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] FTCS, 1998, pp:458-463 [Conf ] Ansgar Fehnker , Edmund M. Clarke , Sumit Kumar Jha , Bruce H. Krogh Refining Abstractions of Hybrid Systems Using Counterexample Fragments. [Citation Graph (0, 0)][DBLP ] HSCC, 2005, pp:242-257 [Conf ] André Platzer , Edmund M. Clarke The Image Computation Problem in Hybrid Systems Model Checking. [Citation Graph (0, 0)][DBLP ] HSCC, 2007, pp:473-486 [Conf ] Sumit Kumar Jha , Bruce H. Krogh , James E. Weimer , Edmund M. Clarke Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction. [Citation Graph (0, 0)][DBLP ] HSCC, 2007, pp:287-300 [Conf ] Christel Baier , Edmund M. Clarke , Vassili Hartonas-Garmhausen , Marta Z. Kwiatkowska , Mark Ryan Symbolic Model Checking for Probabilistic Processes. [Citation Graph (0, 0)][DBLP ] ICALP, 1997, pp:430-440 [Conf ] E. Allen Emerson , Edmund M. Clarke Characterizing Correctness Properties of Parallel Programs Using Fixpoints. [Citation Graph (0, 0)][DBLP ] ICALP, 1980, pp:169-181 [Conf ] Pankaj Chauhan , Edmund M. Clarke , Somesh Jha , James H. Kukula , Thomas R. Shiple , Helmut Veith , Dong Wang Non-linear Quantification Scheduling in Image Computation. [Citation Graph (0, 0)][DBLP ] ICCAD, 2001, pp:293-0 [Conf ] Edmund M. Clarke , Masahiro Fujita , Xudong Zhao Hybrid decision diagrams. [Citation Graph (0, 0)][DBLP ] ICCAD, 1995, pp:159-163 [Conf ] Daniel Kroening , Edmund M. Clarke Checking consistency of C and Verilog using predicate abstraction and induction. [Citation Graph (0, 0)][DBLP ] ICCAD, 2004, pp:66-72 [Conf ] Sérgio Vale Aguiar Campos , Edmund M. Clarke , Wilfredo R. Marrero , Marius Minea Verifying the performance of the PCI local bus using symbolic techniques. [Citation Graph (0, 0)][DBLP ] ICCD, 1995, pp:72-78 [Conf ] Edmund M. Clarke , Daniel Kroening , Karen Yorav Specifying and Verifying Systems with Multiple Clocks. [Citation Graph (0, 0)][DBLP ] ICCD, 2003, pp:48-0 [Conf ] Anubhav Gupta , Edmund M. Clarke Reconsidering CEGAR: Learning Good Abstractions without Refinement. [Citation Graph (0, 0)][DBLP ] ICCD, 2005, pp:591-598 [Conf ] Somesh Jha , Yuan Lu , Marius Minea , Edmund M. Clarke Equivalence Checking Using Abstract BDDs. [Citation Graph (0, 0)][DBLP ] ICCD, 1997, pp:332-337 [Conf ] Samir Sapra , Michael Theobald , Edmund M. Clarke SAT-Based Algorithms for Logic Minimization. [Citation Graph (0, 0)][DBLP ] ICCD, 2003, pp:510-0 [Conf ] Edmund M. Clarke , Daniel Kroening Tutorial: Software Model Checking. [Citation Graph (0, 0)][DBLP ] ICFEM, 2004, pp:9-10 [Conf ] Daniel Kroening , Alex Groce , Edmund M. Clarke Counterexample Guided Abstraction Refinement Via Program Execution. [Citation Graph (0, 0)][DBLP ] ICFEM, 2004, pp:224-238 [Conf ] Alexis Campailla , Sagar Chaki , Edmund M. Clarke , Somesh Jha , Helmut Veith Efficient Filtering in Publish-Subscribe Systems Using Binary Decision. [Citation Graph (0, 0)][DBLP ] ICSE, 2001, pp:443-452 [Conf ] Sagar Chaki , Edmund M. Clarke , Alex Groce , Somesh Jha , Helmut Veith Modular Verification of Software Components in C. [Citation Graph (0, 0)][DBLP ] ICSE, 2003, pp:385-395 [Conf ] Sagar Chaki , Edmund M. Clarke , Orna Grumberg , Joël Ouaknine , Natasha Sharygina , Tayssir Touili , Helmut Veith State/Event Software Verification for Branching-Time Specifications. [Citation Graph (0, 0)][DBLP ] IFM, 2005, pp:53-69 [Conf ] Sagar Chaki , Edmund M. Clarke , Joël Ouaknine , Natasha Sharygina , Nishant Sinha State/Event-Based Software Model Checking. [Citation Graph (0, 0)][DBLP ] IFM, 2004, pp:128-147 [Conf ] Masahiro Fujita , Jerry Chih-Yuan Yang , Edmund M. Clarke , Xudong Zhao , Patrick C. McGeer Fast Spectrum Computation for Logic Functions using Binary Decision Diagrams. [Citation Graph (0, 0)][DBLP ] ISCAS, 1994, pp:275-278 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] Workshop on Languages, Compilers, & Tools for Real-Time Systems, 1995, pp:70-78 [Conf ] Soumitra Bose , Edmund M. Clarke , David E. Long , Spiro Michaylov PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses [Citation Graph (0, 0)][DBLP ] LICS, 1989, pp:80-89 [Conf ] Jerry R. Burch , Edmund M. Clarke , Kenneth L. McMillan , David L. Dill , L. J. Hwang Symbolic Model Checking: 10^20 States and Beyond [Citation Graph (0, 0)][DBLP ] LICS, 1990, pp:428-439 [Conf ] Edmund M. Clarke Automatic Verification of Finite-State Concurrent Systems [Citation Graph (0, 0)][DBLP ] LICS, 1994, pp:126- [Conf ] Edmund M. Clarke , Somesh Jha , Yuan Lu , Helmut Veith Tree-Like Counterexamples in Model Checking. [Citation Graph (0, 0)][DBLP ] LICS, 2002, pp:19-29 [Conf ] Edmund M. Clarke , David E. Long , Kenneth L. McMillan Compositional Model Checking [Citation Graph (0, 0)][DBLP ] LICS, 1989, pp:353-362 [Conf ] Steven M. German , Edmund M. Clarke , Joseph Y. Halpern True Relative Completeness of an Axiom System for the Language L4 (Abridged) [Citation Graph (0, 0)][DBLP ] LICS, 1986, pp:11-25 [Conf ] Edmund M. Clarke , E. Allen Emerson Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. [Citation Graph (0, 0)][DBLP ] Logic of Programs, 1981, pp:52-71 [Conf ] Edmund M. Clarke , Bud Mishra Automatic Verification of Asynchronous Circuits. [Citation Graph (0, 0)][DBLP ] Logic of Programs, 1983, pp:101-115 [Conf ] Steven M. German , Edmund M. Clarke , Joseph Y. Halpern Reasoning About Procedures as Parameters. [Citation Graph (0, 0)][DBLP ] Logic of Programs, 1983, pp:206-220 [Conf ] Sagar Chaki , Edmund M. Clarke , Joël Ouaknine , Natasha Sharygina Automated, compositional and iterative deadlock detection. [Citation Graph (0, 0)][DBLP ] MEMOCODE, 2004, pp:201-210 [Conf ] Edmund M. Clarke , Orna Grumberg , Muralidhar Talupur , Dong Wang High Level Verification of Control Intensive Systems Using Predicate Abstraction. [Citation Graph (0, 0)][DBLP ] MEMOCODE, 2003, pp:55-64 [Conf ] Himanshu Jain , Daniel Kroening , Edmund M. Clarke Verification of SpecC using predicate abstraction. [Citation Graph (0, 0)][DBLP ] MEMOCODE, 2004, pp:7-16 [Conf ] Edmund M. Clarke , Xudong Zhao Word Level Model Checking (Abstract). [Citation Graph (0, 0)][DBLP ] MFCS, 1996, pp:1- [Conf ] Edmund M. Clarke , Orna Grumberg , David E. Long Model checking. [Citation Graph (0, 0)][DBLP ] NATO ASI DPD, 1996, pp:305-349 [Conf ] Edmund M. Clarke , Orna Grumberg , Michael C. Browne Reasoning About Networks With Many Identical Finite-State Processes. [Citation Graph (0, 0)][DBLP ] PODC, 1986, pp:240-248 [Conf ] A. Prasad Sistla , Edmund M. Clarke , Nissim Francez , Yuri Gurevich Can Message Buffers be Characterized in Linear Temporal Logic? [Citation Graph (0, 0)][DBLP ] PODC, 1982, pp:148-156 [Conf ] Edmund M. Clarke Programming Language Constructs for Which it is Impossible to Obtain "Good" Hoare-Like Axiom Systems. [Citation Graph (0, 0)][DBLP ] POPL, 1977, pp:10-20 [Conf ] Edmund M. Clarke Synthesis of Resource Invariants for Concurrent Programs. [Citation Graph (0, 0)][DBLP ] POPL, 1979, pp:211-221 [Conf ] Edmund M. Clarke , E. Allen Emerson , A. Prasad Sistla Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. [Citation Graph (0, 0)][DBLP ] POPL, 1983, pp:117-126 [Conf ] Edmund M. Clarke , Steven M. German , Joseph Y. Halpern On Effective Axiomatizations of Hoare Logics. [Citation Graph (0, 0)][DBLP ] POPL, 1982, pp:309-321 [Conf ] Edmund M. Clarke , Orna Grumberg , David E. Long Model Checking and Abstraction. [Citation Graph (0, 0)][DBLP ] POPL, 1992, pp:342-354 [Conf ] Edmund M. Clarke , Somesh Jha , Wilfredo R. Marrero Using state space exploration and a natural deduction style message derivation engine to verify security protocols. [Citation Graph (0, 0)][DBLP ] PROCOMET, 1998, pp:87-106 [Conf ] Vaibhav Mehta , Constantinos Bartzis , Haifeng Zhu , Edmund M. Clarke , Jeannette M. Wing Ranking Attack Graphs. [Citation Graph (0, 0)][DBLP ] RAID, 2006, pp:127-144 [Conf ] Edmund M. Clarke , I. A. Draghicescu Expressibility results for linear-time and branching-time logics. [Citation Graph (0, 0)][DBLP ] REX Workshop, 1988, pp:428-437 [Conf ] Edmund M. Clarke , Orna Grumberg , David E. Long Verification Tools for Finite-State Concurrent Systems. [Citation Graph (0, 0)][DBLP ] REX School/Symposium, 1993, pp:124-175 [Conf ] Sérgio Vale Aguiar Campos , Edmund M. Clarke , Wilfredo R. Marrero , Marius Minea , Hiromi Hiraishi Computing Quantitative Characteristics of Finite-State Real-Time Systems. [Citation Graph (0, 0)][DBLP ] IEEE Real-Time Systems Symposium, 1994, pp:266-270 [Conf ] Himanshu Jain , Constantinos Bartzis , Edmund M. Clarke Satisfiability Checking of Non-clausal Formulas Using General Matings. [Citation Graph (0, 0)][DBLP ] SAT, 2006, pp:75-89 [Conf ] Edmund M. Clarke , Muralidhar Talupur , Helmut Veith , Dong Wang SAT Based Predicate Abstraction for Hardware Verification. [Citation Graph (0, 0)][DBLP ] SAT, 2003, pp:78-92 [Conf ] Edmund M. Clarke Temporal Logic Model Checking (Abstract). [Citation Graph (0, 0)][DBLP ] ILPS, 1997, pp:3- [Conf ] Edmund M. Clarke SAT-Based Counterexample Guided Abstraction Refinement. [Citation Graph (0, 0)][DBLP ] SPIN, 2002, pp:1- [Conf ] A. Prasad Sistla , Edmund M. Clarke The Complexity of Propositional Linear Temporal Logics [Citation Graph (0, 0)][DBLP ] STOC, 1982, pp:159-168 [Conf ] Edmund M. Clarke , Sergey Berezin Model Checking: Historical Perspective and Example (Extended Abstract). [Citation Graph (0, 0)][DBLP ] TABLEAUX, 1998, pp:18-24 [Conf ] Edmund M. Clarke , Ansgar Fehnker , Zhi Han , Bruce H. Krogh , Olaf Stursberg , Michael Theobald Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. [Citation Graph (0, 0)][DBLP ] TACAS, 2003, pp:192-207 [Conf ] Edmund M. Clarke , Somesh Jha , Wilfredo R. Marrero Partial Order Reductions for Security Protocol Verification. [Citation Graph (0, 0)][DBLP ] TACAS, 2000, pp:503-518 [Conf ] Edmund M. Clarke , Daniel Kroening , Flavio Lerda A Tool for Checking ANSI-C Programs. [Citation Graph (0, 0)][DBLP ] TACAS, 2004, pp:168-176 [Conf ] Edmund M. Clarke , Daniel Kroening , Natasha Sharygina , Karen Yorav SATABS: SAT-Based Predicate Abstraction for ANSI-C. [Citation Graph (0, 0)][DBLP ] TACAS, 2005, pp:570-574 [Conf ] Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu Symbolic Model Checking without BDDs. [Citation Graph (0, 0)][DBLP ] TACAS, 1999, pp:193-207 [Conf ] Sagar Chaki , Edmund M. Clarke , Nicholas Kidd , Thomas W. Reps , Tayssir Touili Verifying Concurrent Message-Passing C Programs with Recursive Calls. [Citation Graph (0, 0)][DBLP ] TACAS, 2006, pp:334-349 [Conf ] Michael C. Browne , Edmund M. Clarke , Orna Grumberg Characterizing Kripke Structures in Temporal Logic. [Citation Graph (0, 0)][DBLP ] TAPSOFT, Vol.1, 1987, pp:256-270 [Conf ] Edmund M. Clarke Counterexample-Guided Abstraction Refinement. [Citation Graph (0, 0)][DBLP ] TIME, 2003, pp:7- [Conf ] Edmund M. Clarke , Orna Grumberg The Model Checking Problem for Concurrent Systems with Many Similar Processes. [Citation Graph (0, 0)][DBLP ] Temporal Logic in Specification, 1987, pp:188-201 [Conf ] Edmund M. Clarke , Himanshu Jain , Nishant Sinha Grand Challenge: Model Check Software. [Citation Graph (0, 0)][DBLP ] VISSAS, 2005, pp:55-68 [Conf ] Jerry R. Burch , Edmund M. Clarke , David E. Long Symbolic Model Checking with Partitioned Transistion Relations. [Citation Graph (0, 0)][DBLP ] VLSI, 1991, pp:49-58 [Conf ] Edmund M. Clarke , Daniel Kroening , Joël Ouaknine , Ofer Strichman Completeness and Complexity of Bounded Model Checking. [Citation Graph (0, 0)][DBLP ] VMCAI, 2004, pp:85-96 [Conf ] Edmund M. Clarke , Muralidhar Talupur , Helmut Veith Environment Abstraction for Parameterized Verification. [Citation Graph (0, 0)][DBLP ] VMCAI, 2006, pp:126-141 [Conf ] Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Ofer Strichman , Yunshan Zhu Bounded model checking. [Citation Graph (0, 0)][DBLP ] Advances in Computers, 2003, v:58, n:, pp:118-149 [Journal ] Edmund M. Clarke Proving Correctness of Coroutines Without History Variables. [Citation Graph (0, 0)][DBLP ] Acta Inf., 1980, v:13, n:, pp:169-188 [Journal ] Edmund M. Clarke , Jeannette M. Wing Formal Methods: State of the Art and Future Directions. [Citation Graph (0, 0)][DBLP ] ACM Comput. Surv., 1996, v:28, n:4, pp:626-643 [Journal ] Edmund M. Clarke , Jeannette M. Wing Tools and Partial Analysis. [Citation Graph (0, 0)][DBLP ] ACM Comput. Surv., 1996, v:28, n:4es, pp:116- [Journal ] Thomas S. Anantharaman , Edmund M. Clarke , Michael J. Foster , Bud Mishra Compiling Path Expressions Into VLSI Circuits. [Citation Graph (0, 0)][DBLP ] Distributed Computing, 1986, v:1, n:3, pp:150-166 [Journal ] Edmund M. Clarke Distributed Computing Issues in Hardware Design. [Citation Graph (0, 0)][DBLP ] Distributed Computing, 1986, v:1, n:4, pp:185-186 [Journal ] Christel Baier , Edmund M. Clarke , Vasilili Hartonas-Garmhausen On the Semantic Foundations of Probabilistic Synchronous Reactive Programs. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 1999, v:22, n:, pp:- [Journal ] Armin Biere , Edmund M. Clarke , Yunshan Zhu Combining Local and Global Model Checking. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 1999, v:23, n:2, pp:- [Journal ] Sérgio Vale Aguiar Campos , Marcio Teixeira , Marius Minea , Andreas Kuehlmann , Edmund M. Clarke Model Checking Semi-Continuous Time Models Using BDDs. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 1999, v:23, n:2, pp:- [Journal ] Sagar Chaki , Joël Ouaknine , Karen Yorav , Edmund M. Clarke Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2003, v:89, n:3, pp:- [Journal ] Edjard Mota , Edmund M. Clarke , Alex Groce , Waleska Oliveira , Marcia Falcão , Jorge Kanda VeriAgent: an Approach to Integrating UML and Formal Verification Tools. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2004, v:95, n:, pp:111-129 [Journal ] Sagar Chaki , Edmund M. Clarke , Joël Ouaknine , Natasha Sharygina , Nishant Sinha Concurrent software verification with states, events, and deadlocks. [Citation Graph (0, 0)][DBLP ] Formal Asp. Comput., 2005, v:17, n:4, pp:461-483 [Journal ] Edmund M. Clarke , Kenneth L. McMillan , Xudong Zhao , Masahiro Fujita , J. Yang Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 1997, v:10, n:2/3, pp:137-148 [Journal ] Edmund M. Clarke , Daniel Kroening , Natasha Sharygina , Karen Yorav Predicate Abstraction of ANSI-C Programs Using SAT. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 2004, v:25, n:2-3, pp:105-127 [Journal ] Edmund M. Clarke , Armin Biere , Richard Raimi , Yunshan Zhu Bounded Model Checking Using Satisfiability Solving. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 2001, v:19, n:1, pp:7-34 [Journal ] 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. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 2002, v:20, n:2, pp:159-186 [Journal ] Edmund M. Clarke , Orna Grumberg , Kiyoharu Hamaguchi Another Look at LTL Model Checking. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 1997, v:10, n:1, pp:47-71 [Journal ] 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. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 1995, v:6, n:2, pp:217-232 [Journal ] Edmund M. Clarke , Steven M. German , Xudong Zhao Verifying the SRT Division Algorithm Using Theorem Proving Techniques. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 1999, v:14, n:1, pp:7-44 [Journal ] Sérgio Vale Aguiar Campos , Edmund M. Clarke , Orna Grumberg Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 2000, v:17, n:2, pp:163-192 [Journal ] Sagar Chaki , Edmund M. Clarke , Alex Groce , Joël Ouaknine , Ofer Strichman , Karen Yorav Efficient Verification of Sequential and Concurrent C Programs. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 2004, v:25, n:2-3, pp:129-166 [Journal ] Edmund M. Clarke Editorial. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 1997, v:10, n:1, pp:5- [Journal ] Edmund M. Clarke , Somesh Jha , Reinhard Enders , Thomas Filkorn Exploiting Symmetry in Temporal Logic Model Checking. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 1996, v:9, n:1/2, pp:77-104 [Journal ] Michael C. Browne , Edmund M. Clarke , Orna Grumberg Reasoning about Networks with Many Identical Finite State Processes [Citation Graph (0, 0)][DBLP ] Inf. Comput., 1989, v:81, n:1, pp:13-31 [Journal ] Steven M. German , Edmund M. Clarke , Joseph Y. Halpern Reasoning about Procedures as Parameters in the Language L4 [Citation Graph (0, 0)][DBLP ] Inf. Comput., 1989, v:83, n:3, pp:265-359 [Journal ] A. Prasad Sistla , Edmund M. Clarke , Nissim Francez , Albert R. Meyer Can Message Buffers Be Axiomatized in Linear Temporal Logic? [Citation Graph (0, 0)][DBLP ] Information and Control, 1984, v:63, n:1/2, pp:88-112 [Journal ] 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. [Citation Graph (0, 0)][DBLP ] Int. J. Found. Comput. Sci., 2003, v:14, n:4, pp:583-604 [Journal ] Edmund M. Clarke , I. A. Draghicescu , Robert P. Kurshan A Unified Approch for Showing Language Inclusion and Equivalence Between Various Types of omega-Automata. [Citation Graph (0, 0)][DBLP ] Inf. Process. Lett., 1993, v:46, n:6, pp:301-308 [Journal ] Edmund M. Clarke , Steven M. German , Joseph Y. Halpern Effective Axiomatizations of Hoare Logics [Citation Graph (0, 0)][DBLP ] J. ACM, 1983, v:30, n:3, pp:612-636 [Journal ] Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith Counterexample-guided abstraction refinement for symbolic model checking. [Citation Graph (0, 0)][DBLP ] J. ACM, 2003, v:50, n:5, pp:752-794 [Journal ] Andrej Bauer , Edmund M. Clarke , Xudong Zhao Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1998, v:21, n:3, pp:295-325 [Journal ] Soumitra Bose , Edmund M. Clarke , David E. Long , Spiro Michaylov PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1992, v:8, n:2, pp:153-181 [Journal ] Sagar Chaki , Edmund M. Clarke , Somesh Jha , Helmut Veith An Iterative Framework for Simulation Conformance. [Citation Graph (0, 0)][DBLP ] J. Log. Comput., 2005, v:15, n:4, pp:465-488 [Journal ] Edmund M. Clarke , Orna Grumberg , Robert P. Kurshan A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems. [Citation Graph (0, 0)][DBLP ] J. Log. Comput., 1992, v:2, n:5, pp:605-618 [Journal ] Sérgio Vale Aguiar Campos , Edmund M. Clarke , Marius Minea Symbolic Techniques for Formally Verifying Industrial Systems. [Citation Graph (0, 0)][DBLP ] Sci. Comput. Program., 1997, v:29, n:1-2, pp:79-98 [Journal ] 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. [Citation Graph (0, 0)][DBLP ] Sci. Comput. Program., 2000, v:36, n:1, pp:53-64 [Journal ] Eric S. Roberts , Arthur Evans Jr. , C. Robert Morgan , Edmund M. Clarke Task Management in Ada-A Critical Evaluation for Real-time Multiprocessors. [Citation Graph (0, 0)][DBLP ] Softw., Pract. Exper., 1981, v:11, n:10, pp:1019-1051 [Journal ] Sérgio Vale Aguiar Campos , Edmund M. Clarke Analysis and Verification of Real-Time Systems Using Quantitative Symbolic Algorithms. [Citation Graph (0, 0)][DBLP ] STTT, 1999, v:2, n:3, pp:260-269 [Journal ] Alessandro Cimatti , Edmund M. Clarke , Fausto Giunchiglia , Marco Roveri NUSMV: A New Symbolic Model Checker. [Citation Graph (0, 0)][DBLP ] STTT, 2000, v:2, n:4, pp:410-425 [Journal ] Edmund M. Clarke , Masahiro Fujita , Sreeranga P. Rajan , Thomas W. Reps , Subash Shankar , Tim Teitelbaum Program slicing for VHDL. [Citation Graph (0, 0)][DBLP ] STTT, 2002, v:4, n:1, pp:125-137 [Journal ] Edmund M. Clarke , Orna Grumberg , Marius Minea , Doron Peled State Space Reduction Using Partial Order Techniques. [Citation Graph (0, 0)][DBLP ] STTT, 1999, v:2, n:3, pp:279-287 [Journal ] Edmund M. Clarke , Somesh Jha , Wilfredo R. Marrero Efficient verification of security protocols using partial-order reductions. [Citation Graph (0, 0)][DBLP ] STTT, 2003, v:4, n:2, pp:173-188 [Journal ] Edmund M. Clarke , Daniel Kroening , Joël Ouaknine , Ofer Strichman Computational challenges in bounded model checking. [Citation Graph (0, 0)][DBLP ] STTT, 2005, v:7, n:2, pp:174-183 [Journal ] Michael C. Browne , Edmund M. Clarke , David L. Dill , Bud Mishra Automatic Verification of Sequential Circuits Using Temporal Logic. [Citation Graph (0, 0)][DBLP ] IEEE Trans. Computers, 1986, v:35, n:12, pp:1035-1044 [Journal ] Edmund M. Clarke , Christos Nikolaou Distributed Reconfiguration Strategies for Fault-Tolerant Multiprocessor Systems. [Citation Graph (0, 0)][DBLP ] IEEE Trans. Computers, 1982, v:31, n:8, pp:771-784 [Journal ] Jerry R. Burch , Edmund M. Clarke , David E. Long , Kenneth L. McMillan , David L. Dill Symbolic model checking for sequential circuit verification. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 1994, v:13, n:4, pp:401-424 [Journal ] Edmund M. Clarke , Yulin Feng Escher-a geometrical layout system for recursively defined circuits. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 1988, v:7, n:8, pp:908-918 [Journal ] Edmund M. Clarke , Anubhav Gupta , Ofer Strichman SAT-based counterexample-guided abstraction refinement. [Citation Graph (0, 0)][DBLP ] IEEE Trans. on CAD of Integrated Circuits and Systems, 2004, v:23, n:7, pp:1113-1123 [Journal ] Michael C. Browne , Edmund M. Clarke , Orna Grumberg Characterizing Finite Kripke Structures in Propositional Temporal Logic. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1988, v:59, n:, pp:115-131 [Journal ] Anca Browne , Edmund M. Clarke , Somesh Jha , David E. Long , Wilfredo R. Marrero An Improved Algorithm for the Evaluation of Fixpoint Expressions. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1997, v:178, n:1-2, pp:237-255 [Journal ] Sérgio Vale Aguiar Campos , Edmund M. Clarke The Verus language: representing time efficiently with BDDs. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 2001, v:253, n:1, pp:95-118 [Journal ] Bhubaneswaru Mishra , Edmund M. Clarke Hierarchical Verification of Asynchronous Circuits Using Temporal Logic. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1985, v:38, n:, pp:269-291 [Journal ] Edmund M. Clarke Synthesis of Resource Invariants for Concurrent Programs. [Citation Graph (0, 0)][DBLP ] ACM Trans. Program. Lang. Syst., 1980, v:2, n:3, pp:338-358 [Journal ] Edmund M. Clarke , Orna Grumberg , Somesh Jha Verifying Parameterized Networks. [Citation Graph (0, 0)][DBLP ] ACM Trans. Program. Lang. Syst., 1997, v:19, n:5, pp:726-750 [Journal ] Edmund M. Clarke , Orna Grumberg , David E. Long Model Checking and Abstraction. [Citation Graph (0, 0)][DBLP ] ACM Trans. Program. Lang. Syst., 1994, v:16, n:5, pp:1512-1542 [Journal ] Edmund M. Clarke , Somesh Jha , Wilfredo R. Marrero Verifying security protocols with Brutus. [Citation Graph (0, 0)][DBLP ] ACM Trans. Softw. Eng. Methodol., 2000, v:9, n:4, pp:443-487 [Journal ] Sagar Chaki , Edmund M. Clarke , Alex Groce , Somesh Jha , Helmut Veith Modular Verification of Software Components in C. [Citation Graph (0, 0)][DBLP ] IEEE Trans. Software Eng., 2004, v:30, n:6, pp:388-402 [Journal ] Nishant Sinha , Edmund M. Clarke SAT-Based Compositional Verification Using Lazy Learning. [Citation Graph (0, 0)][DBLP ] CAV, 2007, pp:39-54 [Conf ] Stephen Magill , Josh Berdine , Edmund M. Clarke , Byron Cook Arithmetic Strengthening for Shape Analysis. [Citation Graph (0, 0)][DBLP ] SAS, 2007, pp:419-436 [Conf ] Himanshu Jain , Daniel Kroening , Natasha Sharygina , Edmund M. Clarke VCEGAR: Verilog CounterExample Guided Abstraction Refinement. [Citation Graph (0, 0)][DBLP ] TACAS, 2007, pp:583-586 [Conf ] Edmund M. Clarke , Himanshu Jain , Daniel Kroening Verification of SpecC using predicate abstraction. [Citation Graph (0, 0)][DBLP ] Formal Methods in System Design, 2007, v:30, n:1, pp:5-28 [Journal ] Model checking algorithms for the µ-calculus. [Citation Graph (, )][DBLP ] The Localization Reduction and Counterexample-Guided Abstraction Refinement. [Citation Graph (, )][DBLP ] Computing Differential Invariants of Hybrid Systems as Fixedpoints. [Citation Graph (, )][DBLP ] Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations. [Citation Graph (, )][DBLP ] Automated Assume-Guarantee Reasoning through Implicit Learning. [Citation Graph (, )][DBLP ] Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway. [Citation Graph (, )][DBLP ] A Bayesian Approach to Model Checking Biological Systems. [Citation Graph (, )][DBLP ] Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts. [Citation Graph (, )][DBLP ] Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. [Citation Graph (, )][DBLP ] Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator. [Citation Graph (, )][DBLP ] Verification of Supervisory Control Software Using State Proximity and Merging. [Citation Graph (, )][DBLP ] Bayesian statistical model checking with application to Simulink/Stateflow verification. [Citation Graph (, )][DBLP ] My 27-year Quest to Overcome the State Explosion Problem. [Citation Graph (, )][DBLP ] Model Checking - My 27-Year Quest to Overcome the State Explosion Problem. [Citation Graph (, )][DBLP ] A Non-prenex, Non-clausal QBF Solver with Game-State Learning. [Citation Graph (, )][DBLP ] The Birth of Model Checking. [Citation Graph (, )][DBLP ] Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic. [Citation Graph (, )][DBLP ] Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. [Citation Graph (, )][DBLP ] Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. [Citation Graph (, )][DBLP ] Learning Minimal Separating DFA's for Compositional Verification. [Citation Graph (, )][DBLP ] Model Checking: Back and Forth between Hardware and Software. [Citation Graph (, )][DBLP ] New and used temporal models: An issue of time. [Citation Graph (, )][DBLP ] Model checking: algorithmic verification and debugging. [Citation Graph (, )][DBLP ] Functional Equivalence Verification Tools in High-Level Synthesis Flows. [Citation Graph (, )][DBLP ] Search in 0.174secs, Finished in 0.188secs