David L. Dill

Formal Methods Syst. Des., February, 2022

Fast and Reliable Formal Verification of Smart Contracts with the Move Prover.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Reasoning About Vectors Using an SMT Theory of Sequences.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 11th International Joint Conference, 2022

2020

Resources: A Safe Language Abstraction for Money.

[BibT_eX]

[DOI]

CoRR, 2020

The Move Prover.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

2019

Learning a SAT Solver from Single-Bit Supervision.

[BibT_eX]

[DOI]

Proceedings of the 7th International Conference on Learning Representations, 2019

The Marabou Framework for Verification and Analysis of Deep Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

2017

Ground-Truth Adversarial Examples.

[BibT_eX]

[DOI]

CoRR, 2017

Towards Proving the Adversarial Robustness of Deep Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the Proceedings First Workshop on Formal Verification of Autonomous Vehicles, 2017

Developing Bug-Free Machine Learning Systems With Formal Mathematics.

[BibT_eX]

[DOI]

Daniel Selsam

Percy Liang

Proceedings of the 34th International Conference on Machine Learning, 2017

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016

CauloBrowser: A systems biology resource for Caulobacter crescentus.

[BibT_eX]

[DOI]

Nucleic Acids Res., 2016

Deciphering cancer biology using boolean methods.

[BibT_eX]

[DOI]

Subarna Sinha

Proceedings of the IEEE International High Level Design Validation and Test Workshop, 2016

2015

Towards in vivo estimation of reaction kinetics using high-throughput metabolomics data: a maximum likelihood approach.

[BibT_eX]

[DOI]

Weiruo Zhang

Ritesh Kolte

BMC Syst. Biol., 2015

2012

Model Checking Cell Biology.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011

Are Cells Asynchronous Circuits? - (Invited Talk).

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2011

Applying a Reusable Election Threat Model at the County Level.

[BibT_eX]

[DOI]

Eric Lazarus

Jeremy Epstein

Proceedings of the 2011 Electronic Voting Technology Workshop / Workshop on Trustworthy Elections, 2011

2010

MiDReG: A method of mining developmentally regulated genes using Boolean implications.

[BibT_eX]

[DOI]

Proc. Natl. Acad. Sci. USA, 2010

Towards program optimization through automated analysis of numerical precision.

[BibT_eX]

[DOI]

Proceedings of the CGO 2010, 2010

2008

EXE: Automatically Generating Inputs of Death.

[BibT_eX]

[DOI]

ACM Trans. Inf. Syst. Secur., 2008

Point/counterpoint: The U.S. should ban paperless electronic voting machines.

[BibT_eX]

[DOI]

Daniel Castro

Commun. ACM, 2008

A Retrospective on Murphi.

[BibT_eX]

[DOI]

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

Automatic Formal Verification of Block Cipher Implementations.

[BibT_eX]

[DOI]

Eric Whitman Smith

Proceedings of the Formal Methods in Computer-Aided Design, 2008

Formal Verification and Biology.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2008

2007

A Decision Procedure for Bit-Vectors and Arrays.

[BibT_eX]

[DOI]

Vijay Ganesh

Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2006

Multiple Representations of Biological Processes.

[BibT_eX]

[DOI]

Carolyn L. Talcott

Trans. Comp. Sys. Biology, 2006

A Refinement Method for Validity Checking of Quantified First-Order Formulas in Hardware Verification.

[BibT_eX]

[DOI]

Husam Abu-Haimed

Proceedings of the Formal Methods in Computer-Aided Design, 6th International Conference, 2006

I Think I Voted: E-Voting vs. Democracy.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

An Incremental Heap Canonicalization Algorithm.

[BibT_eX]

[DOI]

Madanlal Musuvathi

Proceedings of the Model Checking Software, 2005

The Pathalyzer: A Tool for Analysis of Signal Transduction Pathways.

[BibT_eX]

[DOI]

Proceedings of the Systems Biology and Regulatory Genomics, 2005

Multi-threaded reachability.

[BibT_eX]

[DOI]

Proceedings of the 42nd Design Automation Conference, 2005

Predictive Reachability Using a Sample-Based Approach.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 2005

A New Reachability Algorithm for Symmetric Multi-processor Architecture.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2005

2004

Guest Editors' Introduction: E-Voting Security.

[BibT_eX]

[DOI]

Aviel D. Rubin

IEEE Secur. Priv., 2004

A Practical Approach to Partial Functions in CVC Lite.

[BibT_eX]

[DOI]

Proceedings of the Selected Papers from the Workshops on Disproving, 2004

Evaluation of voting systems.

[BibT_eX]

[DOI]

Commun. ACM, 2004

The battle of accountable voting systems.

[BibT_eX]

[DOI]

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

A Partitioning Methodology for BDD-Based Verification.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

Using Interface Refinement to Integrate Formal Verification into the Design Cycle.

[BibT_eX]

[DOI]

Jacob Chang

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

Voting and technology: who gets to count your vote?

[BibT_eX]

[DOI]

Bruce Schneier

Barbara Simons

Commun. ACM, 2003

An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic.

[BibT_eX]

[DOI]

Vijay Ganesh

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

Event Correlation: Language and Semantics.

[BibT_eX]

[DOI]

César Sánchez

Sriram Sankaranarayanan

Proceedings of the Embedded Software, Third International Conference, 2003

Evolution as Design Engineer.

[BibT_eX]

[DOI]

Patrick Lincoln

Proceedings of the Computational Methods in Systems Biology, First International Workshop, 2003

Semi-formal Verification of Memory Systems by Symbolic Simulation.

[BibT_eX]

[DOI]

Husam Abu-Haimed

Proceedings of the Correct Hardware Design and Verification Methods, 2003

Strengthening Invariants by Symbolic Consistency Testing.

[BibT_eX]

[DOI]

Husam Abu-Haimed

Proceedings of the Computer Aided Verification, 15th International Conference, 2003

2002

Formal Verification of Out-of-Order Execution with Incremental Flushing.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2002

Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Logical Frameworks and Meta-Languages, 2002

Using Formal Specifications for Functional Validation of Hardware Designs.

[BibT_eX]

[DOI]

IEEE Des. Test Comput., 2002

Model checking system software with CMC.

[BibT_eX]

[DOI]

Proceedings of the 10th ACM SIGOPS European Workshop, Saint-Emilion, France, July 1, 2002, 2002

CMC: A Pragmatic Approach to Model Checking Real Code.

[BibT_eX]

[DOI]

Proceedings of the 5th Symposium on Operating System Design and Implementation (OSDI 2002), 2002

A Generalization of Shostak's Method for Combining Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 4th International Workshop, 2002

Deciding Presburger Arithmetic by Model Checking and Comparisons with Other Methods.

[BibT_eX]

[DOI]

Vijay Ganesh

Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

Counter-Example Based Predicate Discovery in Predicate Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

Deriving a simulation input generator and a coverage metric from a formal specification.

[BibT_eX]

[DOI]

Proceedings of the 39th Design Automation Conference, 2002

Formal verification methods: getting around the brick wall.

[BibT_eX]

[DOI]

Proceedings of the 39th Design Automation Conference, 2002

CVC: A Cooperating Validity Checker.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 14th International Conference, 2002

Faster Proof Checking in the Edinburgh Logical Framework.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2002

2001

Parallelizing the Murj Verifier.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2001

A Decision Procedure for an Extensional Theory of Arrays.

[BibT_eX]

[DOI]

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

Successive Approximation of Abstract Transition Relations.

[BibT_eX]

[DOI]

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

A simple method for extracting models for protocol code.

[BibT_eX]

[DOI]

Proceedings of the 28th Annual International Symposium on Computer Architecture, 2001

A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® ItaniumTM Processor Bus Protocol.

[BibT_eX]

[DOI]

Ching-Tsun Chou

Proceedings of the Correct Hardware Design and Verification Methods, 2001

2000

Automatic checking of aggregation abstractions through stateenumeration.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2000

Java Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Fifteenth IEEE International Conference on Automated Software Engineering, 2000

Model checking Java programs (abstract only).

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Software Testing and Analysis, 2000

Counterexample-Guided Choice of Projections in Approximate Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 2000 IEEE/ACM International Conference on Computer-Aided Design, 2000

Model checking Java programs.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Formal Methods in Software Practice, 2000

Symbolic Simulation with Approximate Values.

[BibT_eX]

[DOI]

Chris Wilson

Randal E. Bryant

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Monitor-Based Formal Specification of PCI.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Reliable verification using symbolic simulation with scalar values.

[BibT_eX]

[DOI]

Chris Wilson

Proceedings of the 37th Conference on Design Automation, 2000

A Framework for Cooperating Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 2000

1999

Automatic synthesis of extended burst-mode circuits. II. (Automaticsynthesis).

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999

Automatic synthesis of extended burst-mode circuits. I.(Specification and hazard-free implementations).

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999

Timing analysis of asynchronous systems using time separation of events.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1999

An Executable Specification and Verifier for Relaxed Memory Order.

[BibT_eX]

[DOI]

IEEE Trans. Computers, 1999

Verifying Systems with Replicated Components in Mur[b.phiv].

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1999

Approximate Symbolic Model Checking using Overlapping Projections.

[BibT_eX]

[DOI]

Proceedings of the First International Workshop on Symbolic Model Checking, 1999

Formal verification meets simulation (tutorial abstract).

[BibT_eX]

[DOI]

Ellen Sentovich

Serdar Tasiran

Proceedings of the 1999 IEEE/ACM International Conference on Computer-Aided Design, 1999

Improved Approximate Reachability Using Auxiliary State Variables.

[BibT_eX]

[DOI]

Jules P. Bergmann

Proceedings of the 36th Conference on Design Automation, 1999

Alternative Approaches to Hardware Verification (abstract).

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

Experience with Predicate Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998

BDD-based synthesis of extended burst-mode controllers.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1998

Verification of Cache Coherence Protocols by Aggregation of Distributed Transactions.

[BibT_eX]

[DOI]

Theory Comput. Syst., 1998

Verification by approximate forward and backward reachability.

[BibT_eX]

[DOI]

Proceedings of the 1998 IEEE/ACM International Conference on Computer-Aided Design, 1998

Static Analysis to Identify Invariants in RSML Specifications.

[BibT_eX]

[DOI]

David Y. W. Park

Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1998

Checking properties of safety critical specifications using efficient decision procedures.

[BibT_eX]

[DOI]

David Y. W. Park

Mats Per Erik Heimdahl

Barbara J. Czerny

Proceedings of the Second Workshop on Formal Methods in Software Practice, 1998

Formally Verifying Data and Control with Weak Reachability Invariants.

[BibT_eX]

[DOI]

Jeffrey X. Su

Proceedings of the Formal Methods in Computer-Aided Design, 1998

Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 1998

Validation with Guided Search of the State Space.

[BibT_eX]

[DOI]

C. Han Yang

Proceedings of the 35th Conference on Design Automation, 1998

Approximate Reachability with BDDs Using Overlapping Projections.

[BibT_eX]

[DOI]

Mark Horowitz

Proceedings of the 35th Conference on Design Automation, 1998

What's Between Simulation and Formal Verification? (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the 35th Conference on Design Automation, 1998

A Decision Procedure for Bit-Vector Arithmetic.

[BibT_eX]

[DOI]

Jeremy R. Levitt

Proceedings of the 35th Conference on Design Automation, 1998

Practical timing analysis of asynchronous circuits using time separation of events.

[BibT_eX]

[DOI]

Proceedings of the IEEE 1998 Custom Integrated Circuits Conference, 1998

Using Magnatic Disk Instead of Main Memory in the Murphi Verifier.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

Formal Verification of Out-of-Order Execution Using Incremental Flushing.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 10th International Conference, 1998

1997

Approximate algorithms for time separation of events.

[BibT_eX]

[DOI]

Proceedings of the 1997 IEEE/ACM International Conference on Computer-Aided Design, 1997

Automatic Checking of Aggregation Abstractions Through State Enumeration.

[BibT_eX]

Proceedings of the Formal Description Techniques and Protocol Specification, 1997

Parallelizing the Murphi Verifier.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 9th International Conference, 1997

Timing Analysis of Extended Burst-Mode Circuits.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC '97), 1997

More Accurate Polynomial-Time Min-Max Timing Simulation.

[BibT_eX]

[DOI]

Proceedings of the 3rd International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC '97), 1997

1996

Better Verification Through Symmetry.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 1996

An Invitation to Formal Methods.

[BibT_eX]

[DOI]

Computer, 1996

Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions.

[BibT_eX]

[DOI]

Proceedings of the 8th Annual ACM Symposium on Parallel Algorithms and Architectures, 1996

A New Scheme for Memory-Efficient Probabilistic Verification.

[BibT_eX]

Proceedings of the Formal Description Techniques IX: Theory, 1996

Automatic Generation of Invariants in Processor Verification.

[BibT_eX]

[DOI]

Jeffrey X. Su

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Self-Consistency Checking.

[BibT_eX]

[DOI]

Carl-Johan H. Seger

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Validity Checking for Combinations of Theories with Equality.

[BibT_eX]

[DOI]

Jeremy R. Levitt

Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

State Reduction Using Reversible Rules.

[BibT_eX]

[DOI]

Proceedings of the 33st Conference on Design Automation, 1996

Protocol Verification by Aggregation of Distributed Transactions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

Verifying Systems with Replicated Components in Murphi.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

The Murphi Verification System.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 8th International Conference, 1996

1995

Exact two-level minimization of hazard-free logic with multiple-input changes.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1995

An Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order).

[BibT_eX]

[DOI]

Proceedings of the 7th Annual ACM Symposium on Parallel Algorithms and Architectures, 1995

Architecture Validation for Processors.

[BibT_eX]

[DOI]

Proceedings of the 22nd Annual International Symposium on Computer Architecture, 1995

A high-performance asynchronous SCSI controller.

[BibT_eX]

[DOI]

Proceedings of the 1995 International Conference on Computer Design (ICCD '95), 1995

Efficient validity checking for processor verification.

[BibT_eX]

[DOI]

Jerry R. Burch

Proceedings of the 1995 IEEE/ACM International Conference on Computer-Aided Design, 1995

Improved probabilistic verification by hash compaction.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 1995

Automatic verification of the SCI cache coherence protocol.

[BibT_eX]

[DOI]

Proceedings of the Correct Hardware Design and Verification Methods, 1995

Verification of Real-Time Systems by Successive Over and Under Approximation.

[BibT_eX]

[DOI]

Howard Wong-Toi

Proceedings of the Computer Aided Verification, 1995

1994

Self-timed logic using Current-Sensing Completion Detection (CSCD).

[BibT_eX]

[DOI]

Mark E. Dean

Mark Horowitz

J. VLSI Signal Process., 1994

A Theory of Timed Automata.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1994

Symbolic model checking for sequential circuit verification.

[BibT_eX]

[DOI]

IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1994

Performance-driven synthesis of asynchronous controllers.

[BibT_eX]

[DOI]

Proceedings of the 1994 IEEE/ACM International Conference on Computer-Aided Design, 1994

New Techniques for Efficient Verification with Implicitly Conjoined BDDs.

[BibT_eX]

[DOI]

Gary York

Proceedings of the 31st Conference on Design Automation, 1994

Hierarchical Models of Synchronous Circuits (Abstract).

[BibT_eX]

[DOI]

Proceedings of the CONCUR '94, 1994

Automatic verification of Pipelined Microprocessor Control.

[BibT_eX]

[DOI]

Jerry R. Burch

Proceedings of the Computer Aided Verification, 6th International Conference, 1994

1993

Model-Checking in Dense Real-time

[BibT_eX]

[DOI]

Inf. Comput., May, 1993

The design of a high-performance cache controller: a case study in asynchronous synthesis.

[BibT_eX]

[DOI]

Integr., 1993

Efficient Verification of Symmetric Concurrent Systems.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1993 International Conference on Computer Design: VLSI in Computers & Processors, 1993

Unifying synchronous/asynchronous state machine synthesis.

[BibT_eX]

[DOI]

Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, 1993

Modeling hierarchical combinational circuits.

[BibT_eX]

[DOI]

Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, 1993

Automatic Technology Mapping for Generalized Fundamental-Mode Asynchronous Designs.

[BibT_eX]

[DOI]

Polly Siegel

Giovanni De Micheli

Proceedings of the 30th Design Automation Conference. Dallas, 1993

Reducing BDD Size by Exploiting Functional Dependencies.

[BibT_eX]

[DOI]

Proceedings of the 30th Design Automation Conference. Dallas, 1993

Efficient Verification with BDDs using Implicitly Conjoined Invariants.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 5th International Conference, 1993

1992

Symbolic Model Checking: 10^20 States and Beyond

[BibT_eX]

[DOI]

Inf. Comput., June, 1992

Specification and Automatic Verification of Self-Timed Queues.

[BibT_eX]

[DOI]

Robert F. Sproull

Formal Methods Syst. Des., 1992

An implementation of three algorithms for timing verification based on automata emptiness.

[BibT_eX]

[DOI]

Proceedings of the Real-Time Systems Symposium, 1992

Synthesis of 3D Asynchronous State Machines.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1992

Practical Asynchronous Controller Design.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1992

Algorithms for Interface Timing Verification.

[BibT_eX]

[DOI]

Kenneth L. McMillan

Proceedings of the Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1992

Protocol Verification as a Hardware Design Aid.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1992 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1992

Automatic synthesis of 3D asynchronous state machines.

[BibT_eX]

[DOI]

Proceedings of the 1992 IEEE/ACM International Conference on Computer-Aided Design, 1992

Minimization of Timed Transition Systems.

[BibT_eX]

[DOI]

Proceedings of the CONCUR '92, 1992

Higher-Level Specification and Verification with BDDs.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, Fourth International Workshop, 1992

Verification with Real-Time COSPAN.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, Fourth International Workshop, 1992

1991

Verifying Automata Specifications of Probabilistic Real-time Systems.

[BibT_eX]

[DOI]

Proceedings of the Real-Time: Theory in Practice, 1991

Synthesis of Asynchronous State Machines Using A Local Clock.

[BibT_eX]

[DOI]

Proceedings of the Proceedings 1991 IEEE International Conference on Computer Design: VLSI in Computer & Processors, 1991

Automatic Synthesis of Locally-Clocked Asynchronous State Machines.

[BibT_eX]

[DOI]

Proceedings of the 1991 IEEE/ACM International Conference on Computer-Aided Design, 1991

Model-Checking for Probabilistic Real-Time Systems (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 18th International Colloquium, 1991

Checking for Language Inclusion Using Simulation Preorders.

[BibT_eX]

[DOI]

Howard Wong-Toi

Proceedings of the Computer Aided Verification, 3rd International Workshop, 1991

1990

Model-Checking for Real-Time Systems

[BibT_eX]

[DOI]

Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990

Formal verification of cache systems using refinement relations.

[BibT_eX]

[DOI]

Paul Loewenstein

Proceedings of the 1990 IEEE International Conference on Computer Design: VLSI in Computers and Processors, 1990

Automata For Modeling Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 17th International Colloquium, 1990

Sequential Circuit Verification Using Symbolic Model Checking.

[BibT_eX]

[DOI]

Proceedings of the 27th ACM/IEEE Design Automation Conference. Orlando, 1990

Synthesizing Processes and Schedulers from Temporal Specifications.

[BibT_eX]

[DOI]

Howard Wong-Toi

Proceedings of the Computer Aided Verification, 2nd International Workshop, 1990

Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic.

[BibT_eX]

[DOI]

Paul Loewenstein

Proceedings of the Computer Aided Verification, 2nd International Workshop, 1990

1989

Complete Trace Structures.

[BibT_eX]

[DOI]

Proceedings of the Hardware Specification, 1989

Automatic verification of speed-independent circuits with Petri net specifications.

[BibT_eX]

[DOI]

Robert F. Sproull

Proceedings of the Computer Design: VLSI in Computers and Processors, 1989

Practicality of state-machine verification of speed-independent circuits.

[BibT_eX]

[DOI]

Proceedings of the 1989 IEEE International Conference on Computer-Aided Design, 1989

Timing Assumptions and Verification of Finite-State Concurrent Systems.

[BibT_eX]

[DOI]

Proceedings of the Automatic Verification Methods for Finite State Systems, 1989

Trace theory for automatic hierarchical verification of speed-independent circuits.

[BibT_eX]