CAV 1991
44 papers
- "On the Fly" Verification of Behavioural Equivalences and Preorders
- A Linear Time Process Algebra
- A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus
- A Proof Assistant for PSF
- A Semantic Driven Method to Check the Finiteness of CCS Processes
- A Top Down Approach to the Formal Specification of SCI Cache Coherence
- A Two-Level Formal Verification Methodology using HOL and COSMOS
- An Action Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems
- An Algebra of Boolean Processes
- An Automata Theoretic Approach to Temporal Logic
- An Automated Proof Technique for Finite-State Machine Equivalence
- An Overview and Synthesis on Timed Process Algebras
- Automatic Temporal Verification of Buffer Systems
- Automating Most Parts of Hardware Proofs in HOL
- Avoiding State Exposion by Composition of Minimal Covering Graphs
- Bounded-memory Algorithms for Verification On-the-fly
- Checking for Language Inclusion Using Simulation Preorders
- Comparing Generic State Machines
- Complexity Results for POMSET Languages
- Compositional Checking of Satisfaction
- Computing Distinguishing Formulas for Branching Bisimulation
- Deciding Properties of Regular Real Time Processes
- Efficient Algorithms for Verification of Equivalences for Probabilistic Processes
- Error Diagnosis in Finite Communicating Systems
- Formal Verification of Speed-Dependent Asynchronous Cicuits Using Symbolic Model Checking of branching Time Regular Temporal Logic
- From Data Structure to Process Structure
- Functional Extension of Symbolic Model Checking
- Generating BDDs for Symbolic Model Checking in CCS
- Integer Programming in the Analysis of Concurrent Systems
- Mechanically Checked Proofs of Kernel Specification
- Mechanically Verifying Safety and Liveness Properties of Delay Insensitive Circuits
- Mechanizing a Proof by Induction of Process Algebrs Specifications in Higher Order Logic
- Minimum and Maximum Delay Problems in Real-Time Systems
- PAM: A Process Algebra Manipulator
- Partial-Order Model Checking: A Guide for the Perplexed
- Silence is Golden: Branching Bisimilarity is Decidable for Context-Free Processes
- Taming Infinite State Spaces
- Temporal Precondition Verification of Design Transformations
- The Concurrency Workbench with Priorities
- The Lotos Model of a Fault Protected System and its Verification Using a Petri Net Based Approach
- Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties
- Using the HOL Prove Assistant for proving the Correctness of term Rewriting Rules reducing Terms of Sequential Behavior
- Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification
- Verifying Properties of HMS Machine Specifications of Real-Time Systems