Edmund M. Clarke | Academic Influence

Edmund M. Clarke's AcademicInfluence.com Rankings

Edmund M. Clarke

Computer Science

#352

World Rank

#365

Historical Rank

#203

USA Rank

Database

#269

World Rank

#280

Historical Rank

#128

USA Rank

computer-science Degrees

Download Badge

Computer Science

Edmund M. Clarke's Degrees

PhD Computer Science Cornell University
Masters Computer Science Duke University
Bachelors Computer Science Duke University

Similar Degrees You Can Earn

Why Is Edmund M. Clarke Influential?

(Suggest an Edit or Addition)

According to Wikipedia, Edmund Melson Clarke, Jr. was an American computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs. He was the FORE Systems Professor of Computer Science at Carnegie Mellon University. Clarke, along with E. Allen Emerson and Joseph Sifakis, received the 2007 ACM Turing Award.

(See a Problem?)

Edmund M. Clarke's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

Model checking (1996) (4615)
Automatic verification of finite-state concurrent systems using temporal logic specifications (1986) (3958)
Symbolic Model Checking: 10^20 States and Beyond (1990) (3253)
Symbolic Model Checking without BDDs (1999) (2516)
Counterexample-guided abstraction refinement (2003) (1806)
NuSMV 2: An OpenSource Tool for Symbolic Model Checking (2002) (1615)
Formal methods: state of the art and future directions (1996) (1560)
Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic (1981) (1534)
A Tool for Checking ANSI-C Programs (2004) (1438)
Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic (2008) (1376)
Model checking and abstraction (1994) (1246)
Counterexample-guided abstraction refinement for symbolic model checking (2003) (1006)
The complexity of propositional linear temporal logics (1982) (827)
NUSMV: a new symbolic model checker (2000) (803)
Symbolic model checking using SAT procedures instead of BDDs (1999) (802)
Bounded Model Checking Using Satisfiability Solving (2001) (793)
Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons (1982) (763)
NUSMV: A New Symbolic Model Verifier (1999) (708)
Symbolic model checking for sequential circuit verification (1993) (597)
Exploiting symmetry in temporal logic model checking (1993) (561)
The complexity of propositional linear temporal logics (1985) (557)
Compositional model checking (1989) (549)
Model checking and abstraction (1992) (538)
Sequential circuit verification using symbolic model checking (1990) (483)
Nusmv version 2: an opensource tool for symbolic model checking (2002) (469)
Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach (1983) (458)
Characterizing Finite Kripke Structures in Propositional Temporal Logic (1988) (454)
Characterizing Correctness Properties of Parallel Programs Using Fixpoints (1980) (445)
Modular verification of software components in C (2004) (388)
dReal: An SMT Solver for Nonlinear Theories over the Reals (2013) (377)
Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping (1993) (348)
Another Look at LTL Model Checking (1994) (337)
Verification Tools for Finite-State Concurrent Systems (1993) (325)
Verification of the Futurebus+ cache coherence protocol (1993) (315)
SATABS: SAT-Based Predicate Abstraction for ANSI-C (2005) (309)
Symbolic Model Checking with Partitioned Transistion Relations (1991) (306)
Behavioral consistency of C and Verilog programs using bounded model checking (2003) (303)
Automatic Veriication of Nite-state Concurrent Systems Using Temporal-logic Speciications. Acm (1993) (295)
Handbook of Model Checking (2018) (280)
Model Checking and the State Explosion Problem (2011) (258)
Efficient generation of counterexamples and witnesses in symbolic model checking (1995) (255)
The Birth of Model Checking (2008) (255)
A Bayesian Approach to Model Checking Biological Systems (2009) (254)
dReach: δ-Reachability Analysis for Hybrid Systems (2015) (254)
Solving QBF with Counterexample Guided Refinement (2012) (239)
Progress on the State Explosion Problem in Model Checking (2001) (238)
Automatic Verification of Sequential Circuits Using Temporal Logic (1986) (226)
Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems (2003) (213)
Predicate Abstraction of ANSI-C Programs Using SAT (2004) (210)
State space reduction using partial order techniques (1999) (205)
Model checking, abstraction, and compositional verification (1993) (202)
Ranking Attack Graphs (2006) (202)
Symbolic Model Checking for Probabilistic Processes (1997) (199)
Computing differential invariants of hybrid systems as fixedpoints (2008) (194)
Representing circuits more efficiently in symbolic model checking (1991) (194)
Modular verification of software components in C (2003) (183)
State/Event-Based Software Model Checking (2004) (182)
Efficient filtering in publish-subscribe systems using binary decision diagrams (2001) (181)
Model Checking for Security Protocols (1997) (177)
Reasoning about networks with many identical finite-state processes (1986) (173)
δ-Complete Decision Procedures for Satisfiability over the Reals (2012) (173)
Compositional Reasoning in Model Checking (1997) (171)
An Improved Algorithm for the Evaluation of Fixpoint Expressions (1994) (168)
Symbolic Model Checking : IO * ’ States and Beyond * (1992) (167)
SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques (2002) (164)
Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems (1979) (162)
Verifying security protocols with Brutus (2000) (160)
Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis (2002) (160)
Avoiding the state explosion problem in temporal logic model checking (1987) (159)
Tree-like counterexamples in model checking (2002) (155)
Bayesian statistical model checking with application to Simulink/Stateflow verification (2010) (153)
Statistical Model Checking for Cyber-Physical Systems (2011) (152)
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study (2009) (143)
Reasoning about Networks with Many Identical Finite State Processes (1989) (141)
Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs (1999) (139)
Completeness and Complexity of Bounded Model Checking (2004) (136)
Using state space exploration and a natural deduction style message derivation engine to verify security protocols (1998) (131)
Symmetry Reductions in Model Checking (1998) (131)
Veryfying Parameterized Networks using Abstraction and Regular Languages (1995) (130)
Bayesian statistical model checking with application to Stateflow/Simulink verification (2013) (128)
Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway (2008) (122)
Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement (2003) (122)
Environment Abstraction for Parameterized Verification (2006) (121)
Expressibility results for linear-time and branching-time logics (1988) (120)
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking (2000) (119)
Automatic verification of asynchronous circuits using temporal logic (1986) (115)
Statistical Model Checking for Markov Decision Processes (2012) (115)
Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data (1980) (105)
Hybrid decision diagrams. Overcoming the limitations of MTBDDs and BMDs (1995) (100)
Automatic verification of finite-state concurrent systems (1994) (100)
Analytica - A Theorem Prover in Mathematica (1992) (100)
Hardware verification using ANSI-C programs as a reference (2003) (97)
Program Slicing of Hardware Description Languages (1999) (94)
Satisfiability modulo ODEs (2013) (93)
Automatic verification of sequential control systems using temporal logic (1992) (91)
Computing quantitative characteristics of finite-state real-time systems (1994) (91)
Word level predicate abstraction and refinement for verifying RTL Verilog (2005) (86)
Arithmetic Strengthening for Shape Analysis (2007) (85)
Verification by Network Decomposition (2004) (84)
The Image Computation Problem in Hybrid Systems Model Checking (2007) (84)
Verifying Concurrent Message-Passing C Programs with Recursive Calls (2006) (82)
Verifying parameterized networks (1997) (82)
A language for compositional specification and verification of finite state hardware controllers (1991) (80)
A parallel algorithm for constructing binary decision diagrams (1990) (80)
Analysis and verification of the HMGB1 signaling pathway (2010) (79)
A Non-prenex, Non-clausal QBF Solver with Game-State Learning (2010) (79)
Automatic Abstraction in SMT-Based Unbounded Software Model Checking (2013) (78)
Real-time symbolic model checking for discrete time models (1994) (78)
A model checker for authentication protocols (1997) (78)
Delta-Decidability over the Reals (2012) (75)
Automated Assume-Guarantee Reasoning for Simulation Conformance (2005) (75)
Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction (2007) (74)
Modular Translation of Statecharts to SMV (2000) (74)
Efficient Verification of Sequential and Concurrent C Programs (2004) (73)
Counterexamples Revisited: Principles, Algorithms, Applications (2003) (73)
Concurrent software verification with states, events, and deadlocks (2005) (71)
Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages (2008) (70)
Multi-Terminal Binary Decision Diagrams and Hybrid Decision Diagrams (1996) (70)
Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification (1998) (68)
Hierarchical Verification of Asynchronous Circuits Using Temporal Logic (1985) (65)
Learning Minimal Separating DFA's for Compositional Verification (2009) (64)
Verifying the SRT Division Algorithm Using Theorem Proving Techniques (1996) (64)
Verus: a tool for quantitative analysis of finite-state real-time systems (1995) (62)
Inferring Invariants in Separation Logic for Imperative List-processing Programs (2005) (62)
Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems (2008) (61)
Predicate Abstraction with Minimum Predicates (2003) (61)
Counterexample Guided Abstraction Refinement Via Program Execution (2004) (60)
Verifying IP-core based system-on-chip designs (1999) (60)
Statistical Verification of Probabilistic Properties with Unbounded Until (2010) (57)
Dynamic Component Substitutability Analysis (2005) (55)
SAT-based counterexample-guided abstraction refinement (2004) (55)
SAT Based Predicate Abstraction for Hardware Verification (2003) (55)
Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking (1996) (55)
Characterizing Kripke Structures in Temporal Logic (1987) (54)
Programming language constructs for which it is impossible to obtain good hoare-like axiom systems (1977) (54)
Computational challenges in bounded model checking (2005) (53)
Hybrid decision diagrams (1995) (52)
Automated Assume-Guarantee Reasoning through Implicit Learning (2010) (52)
ProbVerus: Probabilistic Symbolic Model Checking (1999) (52)
Verifying Safety Properties of a PowerPC TM 1 Microprocessor Using Symbolic Model Checking without BDDs (1999) (50)
Assume-Guarantee Abstraction Refinement for Probabilistic Systems (2012) (50)
Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach (2003) (50)
Verifying the performance of the PCI local bus using symbolic techniques (1995) (48)
Word Level Symbolic Model Checking: A New Approach for Verifying Arithmetic Circuits (1995) (47)
A Unified Approach For Showing Language Containment And Equivalence Between Various Types Of Omega-Automata (1990) (47)
Verification of a safety-critical railway interlocking system with real-time constraints (1998) (46)
Model checking and theorem proving: a unified framework (2002) (46)
On simulation-based probabilistic model checking of mixed-analog circuits (2010) (45)
Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems (2010) (45)
Using SAT based image computation for reachability analysis (2003) (44)
Parthenon: A parallel theorem prover for non-horn clauses (1988) (43)
Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations (2008) (42)
Verification of evolving software via component substitutability analysis (2008) (41)
Partial Order Reductions for Security Protocol Verification (2000) (41)
Delta-Complete Analysis for Bounded Reachability of Hybrid Systems (2014) (41)
Rare-event verification for stochastic hybrid systems (2012) (41)
The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems (1997) (39)
Verification of SpecC using predicate abstraction (2004) (39)
Analytica – An Experiment in Combining Theorem Proving and Symbolic Computation (1998) (38)
Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator (2009) (38)
Refining Abstractions of Hybrid Systems Using Counterexample Fragments (2005) (38)
Symbolic model checking: 10/sup 20/ states and beyond (1990) (37)
Verification of Supervisory Control Software Using State Proximity and Merging (2008) (37)
A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems (1989) (36)
Symmetry and Induction in Model Checking (1995) (36)
A quantitative approach to the formal verification of real-time systems (1996) (36)
Effective Axiomatizations of Hoare Logics (1983) (36)
Computer Aided Verification (1998) (35)
Program slicing for VHDL (2002) (35)
Automatic verification of sequential circuit designs (1992) (34)
Word level model checking—avoiding the Pentium FDIV error (1996) (33)
SAT-Based Counterexample Guided Abstraction Refinement (2002) (33)
Statistical Model Checking for (2012) (32)
Model Cheking (1997) (32)
SAT-Based Compositional Verification Using Lazy Learning (2007) (32)
A transcriptome analysis by lasso penalized Cox regression for pancreatic cancer survival. (2011) (31)
State/Event Software Verification for Branching-Time Specifications (2005) (31)
SAT-based algorithms for logic minimization (2003) (31)
Can Message Buffers Be Axiomatized in Linear Temporal Logic? (1986) (31)
Synthesis of resource invariants for concurrent programs (1979) (31)
Using Temporal Logic for Automatic Verification of Finite State Systems (1989) (31)
Nonlinear quantification scheduling in image computation (2001) (30)
Automatic Verification of Asynchronous Circuits (1983) (30)
SML-a high level language for the design and verification of finite state machines (1985) (30)
25 Years of Model Checking (2014) (29)
Computational Modeling and Verification of Signaling Pathways in Cancer (2010) (29)
Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System (1996) (29)
Program invariants as fixed points (1977) (29)
Learning abstractions for model checking (2006) (29)
Task management in Ada—A critical evaluation for real‐time multiprocessors (1981) (28)
Fast spectrum computation for logic functions using binary decision diagrams (1994) (28)
Automated, compositional and iterative deadlock detection (2004) (28)
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog (2008) (28)
Model Checking: Software and Beyond (2007) (27)
MODEL CHECKING OF ROBOTIC CONTROL SYSTEMS (2005) (26)
Functional Equivalence Verification Tools in High-Level Synthesis Flows (2009) (25)
Partial order reduction for verification of timed systems (1999) (25)
A Unified Approch for Showing Language Inclusion and Equivalence Between Various Types of omega-Automata (1993) (25)
A SAT-based algorithm for reparameterization in symbolic simulation (2004) (25)
The characterization problem for Hoare logics (1984) (25)
Timing analysis of industrial real-time systems (1995) (24)
Pathway-gene identification for pancreatic cancer survival via doubly regularized Cox regression (2014) (24)
Using Combinatorial Optimization Methods for Quantification Scheduling (2001) (24)
Proving correctness of coroutines without history variables (1978) (23)
Using cutwidth to improve symbolic simulation and Boolean satisfiability (2001) (23)
Checking consistency of C and Verilog using predicate abstraction and induction (2004) (23)
Satisfiability Checking of Non-clausal Formulas Using General Matings (2006) (23)
On effective axiomatizations of Hoare logics (1982) (23)
Reasoning About Procedures as Parameters (1983) (23)
My 27-year Quest to Overcome the State Explosion Problem (2008) (23)
Model checking in-the-loop: Finding counterexamples by systematic simulation (2008) (23)
Applications of Multi-Terminal Binary Decision Diagrams (1995) (23)
Analysis and verification of real-time systems using quantitative symbolic algorithms (1999) (23)
Synthesis of Resource Invariants for Concurrent Programs (1980) (22)
From non-preemptive to preemptive scheduling using synchronization synthesis (2015) (21)
Executable Protocol Specification in ESL (2000) (21)
Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts (2009) (21)
A Machine Checkable Logic of Knowledge forSpecifying Security Properties of ElectronicCommerce Protocols (1998) (21)
Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function (2002) (21)
Formal analysis for logical models of pancreatic cancer (2011) (20)
Abstract BDDs: A Technique for Using Abstraction in Model Checking (1999) (20)
Learning Probabilistic Systems from Tree Samples (2012) (20)
SReach: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems (2015) (20)
Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan (1994) (20)
VeriAgent: an Approach to Integrating UML and Formal Verification Tools (2004) (20)
Multiple State and Single State Tableaux for Combining Local and Global Model Checking (1999) (20)
Reasoning about Procedures as Parameters in the Language L4 (1989) (20)
The Verus language: representing time efficiently with BDDs (1997) (20)
Computer-Aided Verification '90 (1991) (19)
Equivalence checking using abstract BDDs (1997) (19)
Model Checking VHDL with CV (1998) (19)
Specifying and verifying systems with multiple clocks (2003) (19)
Formal Modeling and Analysis of Pancreatic Cancer Microenvironment (2016) (19)
Predicate abstraction and refinement techniques for verifying Verilog (2004) (18)
Towards personalized prostate cancer therapy using delta-reachability analysis (2014) (18)
Teaching cardiac electrophysiology modeling to undergraduate students: laboratory exercises and GPU programming for the study of arrhythmias and spiral wave dynamics. (2011) (18)
Model Checking: Back and Forth between Hardware and Software (2005) (18)
Program invariants as fixedpoints (1979) (17)
Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates (2003) (17)
ANSI-C Bounded Model Checker User Manual (2003) (17)
High level verification of control intensive systems using predicate abstraction (2003) (17)
VCEGAR: Verilog CounterExample Guided Abstraction Refinement (2007) (17)
Analysis and Verification Challenges for Cyber-Physical Transportation Systems (2008) (16)
Error explanation and fault localization with distance metrics (2005) (16)
Can message buffers be characterized in linear temporal logic? (1982) (16)
Studies of biological networks with statistical model checking: application to immune system cells (2013) (16)
Parameter Synthesis for Cardiac Cell Hybrid Models Using δ-Decisions (2014) (16)
Temporal-logics as query languages for dynamic Bayesian networks: application to D. melanogaster embryo development (2006) (16)
The Localization Reduction and Counterexample-Guided Abstraction Refinement (2010) (16)
The Algebraic Mu-Calculus and MTBDDs (1998) (15)
Deadlock prevention in flexible manufacturing systems using symbolic model checking (1996) (15)
Efficient verification of security protocols using partial-order reductions (2003) (15)
Distributed Reconfiguration Strategies for Fault-Tolerant Multiprocessor Systems (1982) (15)
Analog circuit verification by statistical model checking (2011) (15)
Compiling path expressions into VLSI circuits (1985) (14)
Quantifier Elimination over Finite Fields Using Gröbner Bases (2011) (14)
Escher--A Geometrical Layout System for Recursively Defined Circuits (1986) (14)
Hybrid spectral transform diagrams (1997) (13)
Automatic verification of industrial designs (1995) (13)
Solving QBF with Free Variables (2013) (13)
Verification using satisfiability checking, predicate abstraction, and craig interpolation (2008) (12)
Efficient variable ordering using aBDD based sampling (2000) (12)
An Abstraction Technique for Real-Time Verification (2007) (12)
Completeness and Incompleteness Theorems for Hoare-like Axiom Systems (1976) (12)
Program Compatibility Approaches (2005) (12)
Temporal Logic Model Checking (2005) (12)
Probabilistic reachability analysis of the tap withdrawal circuit in caenorhabditis elegans (2016) (11)
Finding Errors in Python Programs Using Dynamic Symbolic Execution (2013) (11)
Model Checking of a Diabetes-Cancer Model (2011) (10)
On the Semantic Foundations of Probabilistic VERUS (1998) (10)
Introduction to Model Checking (2018) (10)
Reconsidering Cegar: learning good abstractions without refinement (2005) (10)
SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems (2016) (10)
Symbolic Techniques for Formally Verifying Industrial Systems (1997) (10)
Counterexample-Guide dAbstractio nRefinemen t ? (2000) (10)
Abstraction techniques for parameterized verification (2006) (10)
Model Checking for Security (1997) (10)
Program Slicing for Design Automation: An Automatic Technique for Speeding-up Hardware Design, Simul (1998) (9)
Proof Generation from Delta-Decisions (2014) (9)
Statistical Model Checking for Complex Stochastic Models in Systems Biology (2009) (9)
Automatic abstraction in model checking (2000) (9)
A Theory of Consistency for Modular Synchronous Systems (2000) (9)
SReach: A Bounded Model Checker for Stochastic Hybrid Systems (2014) (9)
Model checking algorithms for the µ-calculus (2000) (9)
Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning (2010) (9)
Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation (1996) (8)
Parallel Symbolic Computation on Shared Memory Multiprocessor (1990) (8)
SAT-Based Counterexample Guided Abstraction Refinement in Model Checking (2003) (8)
Bayesian statistical model checking with application to Stateflow/Simulink verification (2013) (8)
Abstraction and Assume-Guarantee Reasoning for Automated Software Verification (2013) (7)
Formal Verification of Autonomous Systems NASA Intelligent Systems Program (2001) (7)
Logics of Programs: Workshop Carnegie Mellon University Pittsburgh, PA, June 6-8, 1983 (1984) (7)
Formal Analysis Provides Parameters for Guiding Hyperoxidation in Bacteria using Phototoxic Proteins (2015) (7)
Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions (2014) (7)
True Relative Completeness of an Axiom System for the Language L4 (Abridged) (1986) (7)
Tools and partial analysis (1996) (6)
Parameter Identification Using δ-Decisions for Biological Hybrid Systems (2014) (6)
System Description: Analytica 2 (2003) (6)
Model checking, 2nd Edition (2018) (6)
SAT Solver Descriptions : CMUSAT-Base and CMUSAT (2007) (6)
Symbolic Model Checking forSequential Circuit Veri cationJ (1993) (6)
Towards Personalized Cancer Therapy Using Delta-Reachability Analysis (2014) (6)
Model Checking: Historical Perspective and Example (Extended Abstract) (1998) (6)
Model Checking Hybrid Systems - (Invited Talk) (2014) (6)
Brutus: a model checker for security protocols (2001) (6)
High-level modeling and verification of cellular signaling (2016) (6)
Proceedings of the Carnegie Mellon Workshop on Logic of Programs (1983) (6)
Formal verification of VHDL: the model checker CV (1998) (6)
Model Checking Semi-Continuous Time Models Using BDDs (2001) (6)
SReach: Combining Statistical Tests and Bounded Model Checking for Nonlinear Hybrid Systems with Parametric Uncertainty (2014) (5)
Combining Local and Global Model Checking (2001) (5)
E cient Veri cation of Parallel Real { Time (1993) (5)
Computer-aided verification '90 : proceedings of a DIMACS workshop, June 18-21, 1990 (1991) (5)
Approximate algorithms for optimization of busy waiting in parallel programs (1979) (5)
The Model Checking Problem for Concurrent Systems with Many Similar Processes (1987) (5)
Program Invariants as Fixed Points (Preliminary Reports) (1977) (5)
Model Checking a Synchronous Diabetes-Cancer Logical Network (2013) (4)
Automated compositional analysis for checking component substitutability (2007) (4)
Bifurcation Analysis of Cardiac Alternans Using \delta -Decidability (2016) (4)
Grand Challenge: Model Check Software (2005) (4)
Word level model checking-avoiding the Pentium FDIV error (1996) (4)
Computer-aided verification : 2nd International Conference, CAV '90, New Brunswick, NJ, USA, June 18-21, 1990 : proceedings (1991) (4)
Formal modeling of biological systems (2016) (3)
Floating-point Bugs in Embedded GNU C Library (2013) (3)
Learning Minimal Separating DFAs for Compositional Verification ? Date : October 3 , 2008 (2008) (3)
The Impact of Multiprocessor Technology on High-Level Language Design. (1979) (3)
δ -Decidability over the Reals ∗ (2012) (3)
Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems with Application to Patient-Specific Cardiac Dynamics and Devices (2014) (3)
Bifurcation Analysis of Cardiac Alternans Using δ-Decidability (2016) (3)
CyberCardia project: Modeling, verification and validation of implantable cardiac devices (2016) (3)
Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers (2010) (3)
SAT-Based Predicate Abstraction of Programs (2005) (3)
Model checking : Historical perspective and example (1998) (3)
A methodology for verifying request processing protocols (1983) (3)
New and used temporal models: An issue of time (1993) (3)
Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem (1990) (2)
An Iterative Framework for Simulation Conformance (2005) (2)
NuSmv : a reimplementation of (2007) (2)
Automatic verification of sequential circuit designs. Discussion (1992) (2)
Temporal Verification of Real-Time Systems (1995) (2)
Software Tools for Technology Transfer Manuscript-nr. State Space Reduction Using Partial Order Techniques (1998) (2)
Program Sli ing for VHDL ? (1999) (2)
Temporal Logic Model Checking (Abstract) (1997) (2)
A counterexample guided abstraction refinement framework for verifying concurrent c programs (2005) (2)
Model checking, 1st Edition (2001) (2)
Characterizing Kripke structures in temporal logic. Interim report (1987) (2)
From non-preemptive to preemptive scheduling using synchronization synthesis (2016) (2)
Delta-Complete Reachability Analysis (Part 1) (2013) (2)
Experiments with SAT-Based Symbolic Simulation Using Reparameterization in the Abstraction Refinement Framework (2004) (2)
On the Semantic Foundations of Probabilistic Synchronous Reactive Programs (1998) (2)
Proceedings of the 2nd International Workshop on Computer Aided Verification (1990) (2)
Perspectives of Systems Informatics - 8th International Andrei Ershov Memorial Conference, PSI 2011, Novosibirsk, Russia, June 27-July 1, 2011, Revised Selected Papers (2012) (1)
Tutorial: Software Model Checking (2004) (1)
Optimizing Solution Quality in Synchronization Synthesis (2015) (1)
Computational challenges in boundedmodel checking ∗ (2005) (1)
A Survey of Abstract BDDs ∗ (2008) (1)
5 Conclusion and Future Work 4 Experimental Results (1995) (1)
Model Checking InThe-Loop (2007) (1)
Revisiting the Complexity of Stability of Continuous and Hybrid Systems (2014) (1)
Verification Tools for Embedded Systems (2001) (1)
Assumption Generation for Asynchronous Systems by Abstraction Refinement (2012) (1)
Distributed computing issues in hardware design (1986) (1)
Improving BDD Variable Ordering Using Abstract BDDs and Sampling (1999) (1)
Automatic verification of hardware and software systems (2000) (1)
AnalyticaV : Towards the Mordell-Weil Theorem (2006) (1)
Model Checking Control Software for Nonlinear Dynamic Systems (2008) (1)
2019-01540-Post-Doctoral Research Visit F / M Compositional verification and synthesis from hybrid specifications (2019) (0)
Extracting Proofs from Branch-and-Prune (2013) (0)
Verification of large industrial circuits using sat based reparameterization and automated abstraction-refinement (2007) (0)
EPSL: Executable Protocol Specification Language (2000) (0)
Combining Decision Diagrams and SAT Procedure sfo rEcien tSymboli cModel Checking (2000) (0)
The Characterization Problem for Hoare Logics [ and Discussion ] (2007) (0)
Basics of Verification (2008) (0)
Analyt ica-- An Experiment in Combining Theorem Proving and Symbolic Computat ion * (0)
6 Experimental Results and Conclusions 5 Comparison with Previous Work (1995) (0)
Model checking for studying temporal behavior in cell differentiation (0)
1 Model Checking and Abstraction * (2015) (0)
ExecutableProtocolSpecificationin ESL (2000) (0)
Modular Veriﬁcation of Software Components in C (cid:3) (2018) (0)
Research Directions in Programming Language Semantics and Formal Program Verification (1981) (0)
Tctl with Freeze Quantiiers Complexity of Reasoning about Real-time (1993) (0)
Review of : Model Checking (2004) (0)
EPSL : E xecutable P rotocol S peciﬁcation L anguage (2000) (0)
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 (2006) (0)
2014 Bower Award and Prize for Achievement in Science presented to Edmund Clarke (2016) (0)
Computable Real Numbers and Why They Are Still Important Today (2012) (0)
Word Level Model Checking (Abstract) (1996) (0)
Executable Protocol Specific ation in ESL (2000) (0)
Workshop Paper Selection Committee (2004) (0)
Students Journey Through Odyssey With Faculty , Staff and Alumni Mentors (0)
Using SAT Procedures for Reachability Analysis (2003) (0)
The Completeness Threshold for BoundedModel Che king ? ? ? (2008) (0)
Figure 15: a Run of the Bouncing-ball Automaton Automatic Veriication of Nite-state Con- Current Systems Using Temporal-logic Speciications. Acm Transactions on Programming Figure 13: Two-pass Approximative Analysis down up Y 0 Z 0 (1994) (0)
Bounded Model Checking 1 (2003) (0)
Elimination over Finite Fields Using Grobner Bases (2011) (0)
Simulation-Based Model Checking for Nondeterministic Systems and Rare Events (2016) (0)
Hardware verification (2003) (0)
Temporal Logics for Distributed Systems - Paradigms and Algorithms (Dagstuhl Seminar 99411) (2021) (0)
Symbolic Model Checking withPartitioned Transition (1991) (0)
System Des ription : Analyti a 2 (2003) (0)
4-2012 δ-Decidability over the Reals (2016) (0)
Lemma 4 given 0 = S 0 0 S 0 #cell #nodes #time(sec) Trans. #reachable States #cell #nodes #time(sec) Trans. #reachable States (1994) (0)
Model checking for studying timing of events in T cell differentiation (2012) (0)
Statistical Analysis of High-Dimensional Data for Pancreatic Cancer (2014) (0)
Proceedings of the 8th international conference on Perspectives of System Informatics (2011) (0)
The Algebraic Mu-Calculus and MTBDDsChristel (1998) (0)
A u t o m a t i c Verification of Hardware and Software Systems (2002) (0)
AD-A 277 568 Another Look at LTL Model Checking (0)
Figure 3: Microprocessor Speciication Bolic Model Checking for Sequential Circuit Veriication. Ieee Transactions on 5 Conclusions and Future Work 4.2 Abstracting the Microprocessor Design 4.1 Proving the Lemmas Using Model-checking (0)
New Course Gives Students “ Decision Tools ” To Become Savvy Entrepreneurs (2008) (0)
Formal Verification of VHDL ¾ The Model Checker CV (1998) (0)
Model Checking for Dependable Software-Intensive Systems (2003) (0)
Turing's Computable Real Numbers and Why They Are Still Important Today (2013) (0)
Three Problem Areas Common to Autonomous and Embedded System (2001) (0)
Turing Lecture from the winners of the 2007 ACM A.M. Turing Award. (2009) (0)
Frameworks and Tools for High-Confidence Design of Adaptive, Distributed Embedded Control Systems. Multi-University Research Initiative on High-Confidence Design for Distributed Embedded Systems (2009) (0)
Istituto per La Ricerca Scientifica E Tecnologica Nusmv: a Reimplementation of Smv Nusmv: a Reimplementation of Smv (1998) (0)
Filling In The Gaps : Efficient Techniques for Real Time Verification (0)
Verification of Infinite-State Systems with Applications to Security: Volume 1 NATO Security through Science Series: Information and Communication Security (Nato Security Through Science) (2006) (0)
Advances in counterexample-guided abstraction refinement (2003) (0)

This paper list is powered by the following services:

Other Resources About Edmund M. Clarke

What Schools Are Affiliated With Edmund M. Clarke?

Edmund M. Clarke is affiliated with the following schools:

Image Attributions

Image Source for Edmund M. Clarke