2018
Introduction to Model Checking.
Proceedings of the Handbook of Model Checking., 2018
Model checking, 2nd Edition.
MIT Press, ISBN: 978-0-262-03883-6, 2018
2017
From non-preemptive to preemptive scheduling using synchronization synthesis.
Formal Methods Syst. Des., 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
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
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
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 Syst. Biol., 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
2<sup>5</sup> 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 Syst. Des., 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
Delta-Complete Decision Procedures for Satisfiability over the Reals
CoRR, 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
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 Syst. Des., 2010
Analysis and verification of the HMGB1 signaling pathway.
BMC Bioinform., 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 Syst. Des., 2009
Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations.
Formal Methods Syst. Des., 2009
Functional Equivalence Verification Tools in High-Level Synthesis Flows.
IEEE Des. Test Comput., 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. Comput. Aided Des. Integr. Circuits Syst., 2008
Verification of evolving software via component substitutability analysis.
Formal Methods Syst. Des., 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
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
Model checking in-the-loop: Finding counterexamples by systematic simulation.
Proceedings of the American Control Conference, 2008
2007
Model Checking: Software and Beyond.
J. Univers. Comput. Sci., 2007
Verification of SpecC using predicate abstraction.
Formal Methods Syst. Des., 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
Proceedings of the Recent Advances in Intrusion Detection, 9th International Symposium, 2006
2005
Computational challenges in bounded model checking.
Int. J. Softw. Tools Technol. Transf., 2005
An Iterative Framework for Simulation Conformance.
J. Log. Comput., 2005
Concurrent software verification with states, events, and deadlocks.
Formal Aspects 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. Comput. Aided Des. Integr. Circuits Syst., 2004
Predicate Abstraction of ANSI-C Programs Using SAT.
Formal Methods Syst. Des., 2004
Efficient Verification of Sequential and Concurrent C Programs.
Formal Methods Syst. Des., 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
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.
Int. J. Softw. Tools Technol. Transf., 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
VeriAgent: an Approach to Integrating UML and Formal Verification Tools.
Proceedings of the 6th Brazilian Workshop on Formal Methods, 2003
Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach.
Proceedings of the 2003 Workshop on Software Model Checking, 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
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.
Int. J. Softw. Tools Technol. Transf., 2002
Verification of Out-Of-Order Processor Designs Using Model Checking and a Light-Weight Completion Function.
Formal Methods Syst. Des., 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 Syst. Des., 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
Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001
Model checking, 1st Edition.
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.
Int. J. Softw. Tools Technol. Transf., 2000
Automatic verification of hardware and software systems.
ACM SIGSOFT Softw. Eng. 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 Syst. Des., 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.
Int. J. Softw. Tools Technol. Transf., 1999
Analysis and Verification of Real-Time Systems Using Quantitative Symbolic Algorithms.
Int. J. Softw. Tools Technol. Transf., 1999
Verifying the SRT Division Algorithm Using Theorem Proving Techniques.
Formal Methods Syst. Des., 1999
Model Checking Semi-Continuous Time Models Using BDDs.
Proceedings of the First International Workshop on Symbolic Model Checking, 1999
Combining Local and Global Model Checking.
Proceedings of the First International Workshop on Symbolic Model Checking, 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. Reason., 1998
On the Semantic Foundations of Probabilistic Synchronous Reactive Programs.
Proceedings of the First International Workshop on Probabilistic Methods in Verification, 1998
Model Checking: Historical Perspective and Example (Extended Abstract).
Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 1998
Formal Verification of VHDL ¾ The Model Checker CV.
Proceedings of the 11th Annual Symposium on Integrated Circuits Design, 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
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 in Model 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 Syst. Des., 1997
Another Look at LTL Model Checking.
Formal Methods Syst. Des., 1997
Formal Methods Syst. Des., 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
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
1996
Exploiting Symmetry in Temporal Logic Model Checking.
Formal Methods Syst. Des., 1996
Tools and Partial Analysis.
ACM Comput. Surv., 1996
Formal Methods: State of the Art and Future Directions.
ACM Comput. Surv., 1996
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
Proceedings of the Computer Aided Verification, 8th International Conference, 1996
1995
Temporal Verification of Real-Time Systems.
IEICE Trans. Inf. Syst., 1995
Verification of the Futurebus+ Cache Coherence Protocol.
Formal Methods Syst. Des., 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. Comput. Aided Des. Integr. Circuits Syst., 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
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
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
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. Reason., 1992
Analytica - A Theorem Prover in Mathematica.
Proceedings of the Automated Deduction, 1992
1991
A language for compositional specification and verification of finite state hardware controllers.
Proc. IEEE, 1991
Symbolic Model Checking with Partitioned Transistion Relations.
Proceedings of the VLSI 91, 1991
Representing Circuits More Efficiently in Symbolic Model Checking.
Proceedings of the 28th Design Automation Conference, 1991
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
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
1988
Characterizing Finite Kripke Structures in Propositional Temporal Logic.
Theor. Comput. Sci., 1988
Escher-a geometrical layout system for recursively defined circuits.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 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 Comput., 1986
Compiling Path Expressions Into VLSI Circuits.
Distributed Comput., 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
1985
The Complexity of Propositional Linear Temporal Logics
J. ACM, July, 1985
Hierarchical Verification of Asynchronous Circuits Using Temporal Logic.
Theor. Comput. Sci., 1985
1984
Can Message Buffers Be Axiomatized in Linear Temporal Logic?
Inf. Control., 1984
Using Temporal Logic for Automatic Verification of Finite State Systems.
Proceedings of the Logics and Models of Concurrent Systems, 1984
1983
Effective Axiomatizations of Hoare Logics
J. ACM, July, 1983
A methodology for verifying request processing protocols.
Proceedings of the symposium on Communications Architectures & Protocols, 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
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. Exp., 1981
1980
Synthesis of Resource Invariants for Concurrent Programs.
ACM Trans. Program. Lang. Syst., 1980
Proving Correctness of Coroutines Without History Variables.
Acta Informatica, 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
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
1976
Completeness and Incompleteness Theorems for Hoare-like Axiom Systems.
PhD thesis, 1976