Edmund M. Clarke

According to our database1, Edmund M. Clarke
  • authored at least 306 papers between 1977 and 2017.
  • has a "Dijkstra number"2 of three.

Awards

Turing Prize recipient

Turing Prize 2007, "For their roles in developing model checking into a highly effective verification technology, widely adopted in the hardware and software industries." awarded to Edmund M. Clarke and E. Allen Emerson and Joseph Sifakis.

ACM Fellow

ACM Fellow 1998, "Edmund M. Clarke is the co-inventor of Model Checking (with his former student Allen Emerson). He and his graduate students helped make Model Checking a tool that can be used to verify finite-state concurrent systems of industrial complexity.".

IEEE Fellow

IEEE Fellow 2005, "For contributions to model checking methods for formal verification.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2017
From non-preemptive to preemptive scheduling using synchronization synthesis.
Formal Methods in System Design, 2017

2016
Solving QBF with counterexample guided refinement.
Artif. Intell., 2016

SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems.
Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, 2016

Formal modeling of biological systems.
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2016

High-level modeling and verification of cellular signaling.
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2016

Probabilistic reachability analysis of the tap withdrawal circuit in caenorhabditis elegans.
Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2016

Formal Modeling and Analysis of Pancreatic Cancer Microenvironment.
Proceedings of the Computational Methods in Systems Biology, 2016

Bifurcation Analysis of Cardiac Alternans Using \delta -Decidability.
Proceedings of the Computational Methods in Systems Biology, 2016

CyberCardia project: Modeling, verification and validation of implantable cardiac devices.
Proceedings of the IEEE International Conference on Bioinformatics and Biomedicine, 2016

2015
Optimizing Solution Quality in Synchronization Synthesis.
CoRR, 2015

From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis.
CoRR, 2015

dReach: δ-Reachability Analysis for Hybrid Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2015

Towards personalized prostate cancer therapy using delta-reachability analysis.
Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 2015

Formal Analysis Provides Parameters for Guiding Hyperoxidation in Bacteria using Phototoxic Proteins.
Proceedings of the 25th edition on Great Lakes Symposium on VLSI, GLVLSI 2015, Pittsburgh, PA, USA, May 20, 2015

SReach: A Probabilistic Bounded Delta-Reachability Analyzer for Stochastic Hybrid Systems.
Proceedings of the Computational Methods in Systems Biology, 2015

From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
SReach: Combining Statistical Tests and Bounded Model Checking for Nonlinear Hybrid Systems with Parametric Uncertainty.
CoRR, 2014

Towards Personalized Cancer Therapy Using Delta-Reachability Analysis.
CoRR, 2014

Parameter Synthesis for Cardiac Cell Hybrid Models Using Delta-Decisions.
CoRR, 2014

Delta-Complete Analysis for Bounded Reachability of Hybrid Systems.
CoRR, 2014

Proof Generation from Delta-Decisions.
CoRR, 2014

Revisiting the Complexity of Stability of Continuous and Hybrid Systems.
CoRR, 2014

Pathway-gene identification for pancreatic cancer survival via doubly regularized Cox regression.
BMC Systems Biology, 2014

Proof Generation from Delta-Decisions.
Proceedings of the 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2014

Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems with Application to Patient-Specific Cardiac Dynamics and Devices.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, 2014

Model Checking Hybrid Systems - (Invited Talk).
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, 2014

25 Years of Model Checking.
Proceedings of the Perspectives of System Informatics, 2014

Parameter Synthesis for Cardiac Cell Hybrid Models Using δ-Decisions.
Proceedings of the Computational Methods in Systems Biology, 2014

2013
Bayesian statistical model checking with application to Stateflow/Simulink verification.
Formal Methods in System Design, 2013

Automatic Abstraction in SMT-Based Unbounded Software Model Checking.
CoRR, 2013

Satisfiability Modulo ODEs.
CoRR, 2013

Turing's Computable Real Numbers and Why They Are Still Important Today.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013

Finding Errors in Python Programs Using Dynamic Symbolic Execution.
Proceedings of the Testing Software and Systems, 2013

Satisfiability modulo ODEs.
Proceedings of the Formal Methods in Computer-Aided Design, 2013

Solving QBF with Free Variables.
Proceedings of the Principles and Practice of Constraint Programming, 2013

Automatic Abstraction in SMT-Based Unbounded Software Model Checking.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

dReal: An SMT Solver for Nonlinear Theories over the Reals.
Proceedings of the Automated Deduction - CADE-24, 2013

Studies of biological networks with statistical model checking: application to immune system cells.
Proceedings of the ACM Conference on Bioinformatics, 2013

2012
Learning Probabilistic Systems from Tree Samples
CoRR, 2012

Assume-Guarantee Abstraction Refinement for Probabilistic Systems
CoRR, 2012

Delta-Decidability over the Reals
CoRR, 2012

Delta-Complete Decision Procedures for Satisfiability over the Reals
CoRR, 2012

Solving QBF with Counterexample Guided Refinement.
Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2012, 2012

Statistical Model Checking for Markov Decision Processes.
Proceedings of the Ninth International Conference on Quantitative Evaluation of Systems, 2012

Learning Probabilistic Systems from Tree Samples.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Delta-Decidability over the Reals.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Rare-event verification for stochastic hybrid systems.
Proceedings of the Hybrid Systems: Computation and Control (part of CPS Week 2012), 2012

Assumption Generation for Asynchronous Systems by Abstraction Refinement.
Proceedings of the Formal Aspects of Component Software, 9th International Symposium, 2012

Assume-Guarantee Abstraction Refinement for Probabilistic Systems.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

δ-Complete Decision Procedures for Satisfiability over the Reals.
Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

Computable Real Numbers and Why They Are Still Important Today.
Proceedings of the ACM Turing Centenary Celebration, 2012

2011
Quantifier Elimination over Finite Fields Using Gröbner Bases
CoRR, 2011

Model Checking and the State Explosion Problem.
Proceedings of the Tools for Practical Software Verification, 2011

Formal analysis for logical models of pancreatic cancer.
Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference, 2011

Quantifier Elimination over Finite Fields Using Gröbner Bases.
Proceedings of the Algebraic Informatics - 4th International Conference, 2011

Statistical Model Checking for Cyber-Physical Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2011

Analog circuit verification by statistical model checking.
Proceedings of the 16th Asia South Pacific Design Automation Conference, 2011

2010
On simulation-based probabilistic model checking of mixed-analog circuits.
Formal Methods in System Design, 2010

Analysis and verification of the HMGB1 signaling pathway.
BMC Bioinformatics, 2010

Statistical Verification of Probabilistic Properties with Unbounded Until.
Proceedings of the Formal Methods: Foundations and Applications, 2010

A Non-prenex, Non-clausal QBF Solver with Game-State Learning.
Proceedings of the Theory and Applications of Satisfiability Testing, 2010

Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010

Bayesian statistical model checking with application to Simulink/Stateflow verification.
Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, 2010

Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems.
Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, 2010

Automated Assume-Guarantee Reasoning through Implicit Learning.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

The Localization Reduction and Counterexample-Guided Abstraction Refinement.
Proceedings of the Time for Verification, 2010

Computational Modeling and Verification of Signaling Pathways in Cancer.
Proceedings of the Algebraic and Numeric Biology - 4th International Conference, 2010

2009
Computing differential invariants of hybrid systems as fixedpoints.
Formal Methods in System Design, 2009

Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations.
Formal Methods in System Design, 2009

Functional Equivalence Verification Tools in High-Level Synthesis Flows.
IEEE Design & Test of Computers, 2009

Model checking: algorithmic verification and debugging.
Commun. ACM, 2009

Learning Minimal Separating DFA's for Compositional Verification.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2009

Model Checking - My 27-year Quest to Overcome the State Explosion Problem.
Proceedings of the First NASA Formal Methods Symposium, 2009

My 27-year Quest to Overcome the State Explosion Problem.
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.
Proceedings of the FM 2009: Formal Methods, 2009

Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts.
Proceedings of the 46th Design Automation Conference, 2009

A Bayesian Approach to Model Checking Biological Systems.
Proceedings of the Computational Methods in Systems Biology, 7th International Conference, 2009

2008
Word-Level Predicate-Abstraction and Refinement Techniques for Verifying RTL Verilog.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2008

Verification of evolving software via component substitutability analysis.
Formal Methods in System Design, 2008

Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic.
Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008

The Birth of Model Checking.
Proceedings of the 25 Years of Model Checking - History, Achievements, Perspectives, 2008

Model Checking - My 27-Year Quest to Overcome the State Explosion Problem.
Proceedings of the Logic for Programming, 2008

Verification of Supervisory Control Software Using State Proximity and Merging.
Proceedings of the Hybrid Systems: Computation and Control, 11th International Workshop, 2008

Statistical Model Checking of Mixed-Analog Circuits with an Application to a Third Order Delta-Sigma Modulator.
Proceedings of the Hardware and Software: Verification and Testing, 2008

Statistical Model Checking in BioLab: Applications to the Automated Analysis of T-Cell Receptor Signaling Pathway.
Proceedings of the Computational Methods in Systems Biology, 6th International Conference, 2008

Computing Differential Invariants of Hybrid Systems as Fixedpoints.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007
Model Checking: Software and Beyond.
J. UCS, 2007

Verification of SpecC using predicate abstraction.
Formal Methods in System Design, 2007

VCEGAR: Verilog CounterExample Guided Abstraction Refinement.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007

Arithmetic Strengthening for Shape Analysis.
Proceedings of the Static Analysis, 14th International Symposium, 2007

The Image Computation Problem in Hybrid Systems Model Checking.
Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction.
Proceedings of the Hybrid Systems: Computation and Control, 10th International Workshop, 2007

SAT-Based Compositional Verification Using Lazy Learning.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006
Environment Abstraction for Parameterized Verification.
Proceedings of the Verification, 2006

Verifying Concurrent Message-Passing C Programs with Recursive Calls.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Satisfiability Checking of Non-clausal Formulas Using General Matings.
Proceedings of the Theory and Applications of Satisfiability Testing, 2006

Ranking Attack Graphs.
Proceedings of the Recent Advances in Intrusion Detection, 9th International Symposium, 2006

2005
Computational challenges in bounded model checking.
STTT, 2005

An Iterative Framework for Simulation Conformance.
J. Log. Comput., 2005

Concurrent software verification with states, events, and deadlocks.
Formal Asp. Comput., 2005

Model Checking: Back and Forth between Hardware and Software.
Proceedings of the Verified Software: Theories, 2005

Grand Challenge: Model Check Software.
Proceedings of the Verification of Infinite-State Systems with Applications to Security, 2005

SATABS: SAT-Based Predicate Abstraction for ANSI-C.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005

State/Event Software Verification for Branching-Time Specifications.
Proceedings of the Integrated Formal Methods, 5th International Conference, 2005

Reconsidering CEGAR: Learning Good Abstractions without Refinement.
Proceedings of the 23rd International Conference on Computer Design (ICCD 2005), 2005

Refining Abstractions of Hybrid Systems Using Counterexample Fragments.
Proceedings of the Hybrid Systems: Computation and Control, 8th International Workshop, 2005

Program Compatibility Approaches.
Proceedings of the Formal Methods for Components and Objects, 4th International Symposium, 2005

Dynamic Component Substitutability Analysis.
Proceedings of the FM 2005: Formal Methods, 2005

Word level predicate abstraction and refinement for verifying RTL verilog.
Proceedings of the 42nd Design Automation Conference, 2005

Automated Assume-Guarantee Reasoning for Simulation Conformance.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Temporal Logic Model Checking.
Proceedings of the Handbook of Networked and Embedded Control Systems, 2005

2004
Modular Verification of Software Components in C.
IEEE Trans. Software Eng., 2004

SAT-based counterexample-guided abstraction refinement.
IEEE Trans. on CAD of Integrated Circuits and Systems, 2004

Predicate Abstraction of ANSI-C Programs Using SAT.
Formal Methods in System Design, 2004

Efficient Verification of Sequential and Concurrent C Programs.
Formal Methods in System Design, 2004

VeriAgent: an Approach to Integrating UML and Formal Verification Tools.
Electr. Notes Theor. Comput. Sci., 2004

Completeness and Complexity of Bounded Model Checking.
Proceedings of the Verification, 2004

A Tool for Checking ANSI-C Programs.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004

Verification of SpecC using predicate abstraction.
Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 2004

Automated, compositional and iterative deadlock detection.
Proceedings of the 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 2004

State/Event-Based Software Model Checking.
Proceedings of the Integrated Formal Methods, 4th International Conference, 2004

Counterexample Guided Abstraction Refinement Via Program Execution.
Proceedings of the Formal Methods and Software Engineering, 2004

Tutorial: Software Model Checking.
Proceedings of the Formal Methods and Software Engineering, 2004

Checking consistency of C and Verilog using predicate abstraction and induction.
Proceedings of the 2004 International Conference on Computer-Aided Design, 2004

A SAT-based algorithm for reparameterization in symbolic simulation.
Proceedings of the 41th Design Automation Conference, 2004

Verification by Network Decomposition.
Proceedings of the CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31, 2004

2003
Efficient verification of security protocols using partial-order reductions.
STTT, 2003

Counterexample-guided abstraction refinement for symbolic model checking.
J. ACM, 2003

Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems.
Int. J. Found. Comput. Sci., 2003

Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach.
Electr. Notes Theor. Comput. Sci., 2003

Bounded model checking.
Advances in Computers, 2003

Counterexample-Guided Abstraction Refinement.
Proceedings of the 10th International Symposium on Temporal Representation and Reasoning / 4th International Conference on Temporal Logic (TIME-ICTL 2003), 2003

Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

SAT Based Predicate Abstraction for Hardware Verification.
Proceedings of the Theory and Applications of Satisfiability Testing, 2003

High Level Verification of Control Intensive Systems Using Predicate Abstraction.
Proceedings of the 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 2003

Modular Verification of Software Components in C.
Proceedings of the 25th International Conference on Software Engineering, 2003

SAT-Based Algorithms for Logic Minimization.
Proceedings of the 21st International Conference on Computer Design (ICCD 2003), 2003

Specifying and Verifying Systems with Multiple Clocks.
Proceedings of the 21st International Conference on Computer Design (ICCD 2003), 2003

Model Checking for Dependable Software-Intensive Systems.
Proceedings of the 2003 International Conference on Dependable Systems and Networks (DSN 2003), 2003

Behavioral consistency of C and verilog programs using bounded model checking.
Proceedings of the 40th Design Automation Conference, 2003

Predicate Abstraction with Minimum Predicates.
Proceedings of the Correct Hardware Design and Verification Methods, 2003

Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003

SAT-Based Counterexample Guided Abstraction Refinement in Model Checking.
Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

Counterexamples Revisited: Principles, Algorithms, Applications.
Proceedings of the Verification: Theory and Practice, 2003

Hardware verification using ANSI-C programs as a reference.
Proceedings of the 2003 Asia and South Pacific Design Automation Conference, 2003

2002
Program slicing for VHDL.
STTT, 2002

Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function.
Formal Methods in System Design, 2002

SAT-Based Counterexample Guided Abstraction Refinement.
Proceedings of the Model Checking of Software, 2002

Tree-Like Counterexamples in Model Checking.
Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002

Automated Abstraction Refinement for Model Checking Large State Spaces Using SAT Based Conflict Analysis.
Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

NuSMV 2: An OpenSource Tool for Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
The Verus language: representing time efficiently with BDDs.
Theor. Comput. Sci., 2001

Bounded Model Checking Using Satisfiability Solving.
Formal Methods in System Design, 2001

Efficient Filtering in Publish-Subscribe Systems Using Binary Decision.
Proceedings of the 23rd International Conference on Software Engineering, 2001

Non-linear Quantification Scheduling in Image Computation.
Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, 2001

Using cutwidth to improve symbolic simulation and Boolean satisfiability.
Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop 2001, 2001

Progress on the State Explosion Problem in Model Checking.
Proceedings of the Informatics - 10 Years Back. 10 Years Ahead., 2001

Using Combinatorial Optimization Methods for Quantification Scheduling.
Proceedings of the Correct Hardware Design and Verification Methods, 2001

Model Checking.
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

Model checking.
MIT Press, ISBN: 978-0-262-03270-4, 2001

2000
Verifying security protocols with Brutus.
ACM Trans. Softw. Eng. Methodol., 2000

NUSMV: A New Symbolic Model Checker.
STTT, 2000

Automatic verification of hardware and software systems.
ACM SIGSOFT Software Engineering Notes, 2000

Verification of a safety-critical railway interlocking system with real-time constraints.
Sci. Comput. Program., 2000

Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System.
Formal Methods in System Design, 2000

Partial Order Reductions for Security Protocol Verification.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

Executable Protocol Specification in ESL.
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

A Theory of Consistency for Modular Synchronous Systems.
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Efficient variable ordering using aBDD based sampling.
Proceedings of the 37th Conference on Design Automation, 2000

Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Counterexample-Guided Abstraction Refinement.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Model checking algorithms for the µ-calculus.
Proceedings of the Proof, Language, and Interaction, Essays in Honour of Robin Milner, 2000

1999
State Space Reduction Using Partial Order Techniques.
STTT, 1999

Analysis and Verification of Real-Time Systems Using Quantitative Symbolic Algorithms.
STTT, 1999

Verifying the SRT Division Algorithm Using Theorem Proving Techniques.
Formal Methods in System Design, 1999

Model Checking Semi-Continuous Time Models Using BDDs.
Electr. Notes Theor. Comput. Sci., 1999

Combining Local and Global Model Checking.
Electr. Notes Theor. Comput. Sci., 1999

On the Semantic Foundations of Probabilistic Synchronous Reactive Programs.
Electr. Notes Theor. Comput. Sci., 1999

Symbolic Model Checking without BDDs.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1999

Symbolic Model Checking Using SAT Procedures instead of BDDs.
Proceedings of the 36th Conference on Design Automation, 1999

Abstract BDDs: A Technique for Using Abstraction in Model Checking.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

Program Slicing of Hardware Description Languages.
Proceedings of the Correct Hardware Design and Verification Methods, 1999

NUSMV: A New Symbolic Model Verifier.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Multiple State and Single State Tableaux for Combining Local and Global Model Checking.
Proceedings of the Correct System Design, 1999

ProbVerus: Probabilistic Symbolic Model Checking.
Proceedings of the Formal Methods for Real-Time and Probabilistic Systems, 1999

1998
Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation.
J. Autom. Reasoning, 1998

Model Checking: Historical Perspective and Example (Extended Abstract).
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1998

Using state space exploration and a natural deduction style message derivation engine to verify security protocols.
Proceedings of the Programming Concepts and Methods, 1998

Verification of a Safety-Critical Railway Interlocking System with Real-Time Constraints.
Proceedings of the Digest of Papers: FTCS-28, 1998

Model Checking VHDL with CV.
Proceedings of the Formal Methods in Computer-Aided Design, 1998

Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification.
Proceedings of the Formal Methods in Computer-Aided Design, 1998

Symmetry Reductions inModel Checking.
Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997
Verifying Parameterized Networks.
ACM Trans. Program. Lang. Syst., 1997

An Improved Algorithm for the Evaluation of Fixpoint Expressions.
Theor. Comput. Sci., 1997

Symbolic Techniques for Formally Verifying Industrial Systems.
Sci. Comput. Program., 1997

Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping.
Formal Methods in System Design, 1997

Another Look at LTL Model Checking.
Formal Methods in System Design, 1997

Editorial.
Formal Methods in System Design, 1997

Temporal Logic Model Checking (Abstract).
Proceedings of the Logic Programming, 1997

Equivalence Checking Using Abstract BDDs.
Proceedings of the Proceedings 1997 International Conference on Computer Design: VLSI in Computers & Processors, 1997

Symbolic Model Checking for Probabilistic Processes.
Proceedings of the Automata, Languages and Programming, 24th International Colloquium, 1997

Model Cheking.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1997

Compositional Reasoning in Model Checking.
Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997

The Verus Language: Representing Time Efficiently with BDDs.
Proceedings of the Transformation-Based Reactive Systems Development, 1997

1996
Exploiting Symmetry in Temporal Logic Model Checking.
Formal Methods in System Design, 1996

Tools and Partial Analysis.
ACM Comput. Surv., 1996

Formal Methods: State of the Art and Future Directions.
ACM Comput. Surv., 1996

Model checking.
Proceedings of the NATO Advanced Study Institute on Deductive Program Design, 1996

Word Level Model Checking (Abstract).
Proceedings of the Mathematical Foundations of Computer Science 1996, 1996

Deadlock prevention in flexible manufacturing systems using symbolic model checking.
Proceedings of the 1996 IEEE International Conference on Robotics and Automation, 1996

Verification of All Circuits in a Floating-Point Unit Using Word-Level Model Checking.
Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Word Level Model Checking - Avoiding the Pentium FDIV Error.
Proceedings of the 33st Conference on Design Automation, 1996

Symbolic Model Checking.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Verifying the SRT Division Algorithm Using Theorem Proving Techniques.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Analytica - An Experiment in Combining Theorem Proving and Symbolic Computation.
Proceedings of the Artificial Intelligence and Symbolic Mathematical Computation, 1996

1995
Temporal Verification of Real-Time Systems.
IEICE Transactions, 1995

Verification of the Futurebus+ Cache Coherence Protocol.
Formal Methods in System Design, 1995

Automatic verification of industrial designs.
Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques, 1995

Timing analysis of industrial real-time systems.
Proceedings of the Workshop on Industrial-Strength Formal Specification Techniques, 1995

Verus: A Tool for Quantitative Analysis of Finite-State Real-Time Systems.
Proceedings of the ACM SIGPLAN 1995 Workshop on Languages, 1995

Verifying the performance of the PCI local bus using symbolic techniques.
Proceedings of the 1995 International Conference on Computer Design (ICCD '95), 1995

Hybrid decision diagrams.
Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, 1995

Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking.
Proceedings of the 32st Conference on Design Automation, 1995

Veryfying Parameterized Networks using Abstraction and Regular Languages.
Proceedings of the CONCUR '95: Concurrency Theory, 1995

Symmetry and Induction in Model Checking.
Proceedings of the Computer Science Today: Recent Trends and Developments, 1995

1994
Model Checking and Abstraction.
ACM Trans. Program. Lang. Syst., 1994

Symbolic model checking for sequential circuit verification.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1994

Computing Quantitative Characteristics of Finite-State Real-Time Systems.
Proceedings of the 15th IEEE Real-Time Systems Symposium (RTSS '94), 1994

Automatic Verification of Finite-State Concurrent Systems
Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Fast Spectrum Computation for Logic Functions using Binary Decision Diagrams.
Proceedings of the 1994 IEEE International Symposium on Circuits and Systems, ISCAS 1994, London, England, UK, May 30, 1994

An Improved Algorithm for the Evaluation of Fixpoint Expressions.
Proceedings of the Computer Aided Verification, 6th International Conference, 1994

Another Look at LTL Model Checking.
Proceedings of the Computer Aided Verification, 6th International Conference, 1994

Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

Automatic Verification of Finite-state Concurrent Systems.
Proceedings of the Application and Theory of Petri Nets 1994, 1994

1993
A Unified Approch for Showing Language Inclusion and Equivalence Between Various Types of omega-Automata.
Inf. Process. Lett., 1993

New and used temporal models: An issue of time.
Appl. Intell., 1993

Verification Tools for Finite-State Concurrent Systems.
Proceedings of the A Decade of Concurrency, Reflections and Perspectives, 1993

Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping.
Proceedings of the 30th Design Automation Conference. Dallas, 1993

Verification of the Futurebus+ Cache Coherence Protocol.
Proceedings of the Computer Hardware Description Languages and their Applications, Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications, 1993

Automatic Verification of Sequential Circuit Designs.
Proceedings of the Computer Hardware Description Languages and their Applications, Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications, 1993

Efficient Verification of Parallel Real-Time Systems.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993

Exploiting Symmetry In Temporal Logic Model Checking.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993

1992
Symbolic Model Checking: 10^20 States and Beyond
Inf. Comput., June, 1992

A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems.
J. Log. Comput., 1992

PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses.
J. Autom. Reasoning, 1992

Model Checking and Abstraction.
Proceedings of the Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1992

Analytica - A Theorem Prover in Mathematica.
Proceedings of the Automated Deduction, 1992

1991
Symbolic Model Checking with Partitioned Transistion Relations.
VLSI, 1991

Representing Circuits More Efficiently in Symbolic Model Checking.
Proceedings of the 28th Design Automation Conference, 1991

1990
Symbolic Model Checking: 10^20 States and Beyond
Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

A parallel algorithm for constructing binary decision diagrams.
Proceedings of the 1990 IEEE International Conference on Computer Design: VLSI in Computers and Processors, 1990

Preface.
Proceedings of the Computer-Aided Verification, 1990

Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem.
Proceedings of the Computer-Aided Verification, 1990

Sequential Circuit Verification Using Symbolic Model Checking.
Proceedings of the 27th ACM/IEEE Design Automation Conference. Orlando, 1990

Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem.
Proceedings of the Computer Aided Verification, 2nd International Workshop, 1990

A Unified Approach For Showing Language Containment And Equivalence Between Various Types Of Omega-Automata.
Proceedings of the CAAP '90, 1990

1989
Reasoning about Procedures as Parameters in the Language L4
Inf. Comput., December, 1989

Reasoning about Networks with Many Identical Finite State Processes
Inf. Comput., April, 1989

Compositional Model Checking
Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989

PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses
Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989

A Synthesis of Two Approaches for Verifying Finite State Concurrent Systems.
Proceedings of the Logic at Botik '89, 1989

1988
Characterizing Finite Kripke Structures in Propositional Temporal Logic.
Theor. Comput. Sci., 1988

Escher-a geometrical layout system for recursively defined circuits.
IEEE Trans. on CAD of Integrated Circuits and Systems, 1988

Expressibility results for linear-time and branching-time logics.
Proceedings of the Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands, May 30, 1988

PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses.
Proceedings of the 9th International Conference on Automated Deduction, 1988

1987
The Model Checking Problem for Concurrent Systems with Many Similar Processes.
Proceedings of the Temporal Logic in Specification, 1987

Characterizing Kripke Structures in Temporal Logic.
Proceedings of the TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1987

Avoiding The State Explosion Problem in Temporal Logic Model Checking.
Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, 1987

1986
Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications.
ACM Trans. Program. Lang. Syst., 1986

Automatic Verification of Sequential Circuits Using Temporal Logic.
IEEE Trans. Computers, 1986

Distributed Computing Issues in Hardware Design.
Distributed Computing, 1986

Compiling Path Expressions Into VLSI Circuits.
Distributed Computing, 1986

Reasoning About Networks With Many Identical Finite-State Processes.
Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing, 1986

True Relative Completeness of an Axiom System for the Language L4 (Abridged)
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

Escher - a geometrical layout system for recursively defined circuits.
Proceedings of the 23rd ACM/IEEE Design Automation Conference. Las Vegas, NV, June, 1986., 1986

1985
The Complexity of Propositional Linear Temporal Logics
J. ACM, July, 1985

Hierarchical Verification of Asynchronous Circuits Using Temporal Logic.
Theor. Comput. Sci., 1985

Compiling Path Expressions into VLSI Circuits.
Proceedings of the Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985

1984
Can Message Buffers Be Axiomatized in Linear Temporal Logic?
Information and Control, 1984

1983
Effective Axiomatizations of Hoare Logics
J. ACM, July, 1983

Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach.
Proceedings of the Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, 1983

Reasoning About Procedures as Parameters.
Proceedings of the Logics of Programs, 1983

Automatic Verification of Asynchronous Circuits.
Proceedings of the Logics of Programs, 1983

1982
Distributed Reconfiguration Strategies for Fault-Tolerant Multiprocessor Systems.
IEEE Trans. Computers, 1982

Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons.
Sci. Comput. Program., 1982

The Complexity of Propositional Linear Temporal Logics
Proceedings of the 14th Annual ACM Symposium on Theory of Computing, 1982

On Effective Axiomatizations of Hoare Logics.
Proceedings of the Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, 1982

Can Message Buffers be Characterized in Linear Temporal Logic?
Proceedings of the ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, 1982

1981
Task Management in Ada-A Critical Evaluation for Real-time Multiprocessors.
Softw., Pract. Exper., 1981

Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic.
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, 1981

1980
Synthesis of Resource Invariants for Concurrent Programs.
ACM Trans. Program. Lang. Syst., 1980

Proving Correctness of Coroutines Without History Variables.
Acta Inf., 1980

Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data.
Proceedings of the Sixth International Conference on Very Large Data Bases, 1980

Characterizing Correctness Properties of Parallel Programs Using Fixpoints.
Proceedings of the Automata, 1980

1979
Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems.
J. ACM, 1979

Program invariants as fixedpoints.
Computing, 1979

Synthesis of Resource Invariants for Concurrent Programs.
Proceedings of the Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, 1979

Approximate Algorithms for Optimization of Busy Waiting in Parallel Programs (Preliminary Report)
Proceedings of the 20th Annual Symposium on Foundations of Computer Science, 1979

1977
Programming Language Constructs for Which it is Impossible to Obtain "Good" Hoare-Like Axiom Systems.
Proceedings of the Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, 1977

Program Invariants as Fixed Points (Preliminary Reports)
Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October, 1977


  Loading...