Using the HOL Prove Assistant for proving the Correctness of term Rewriting Rules reducing Terms of Sequential Behavior
Abstract elided by the publisher.
2,069 papers · page 102 of 104
Mechanizing a Proof by Induction of Process Algebrs Specifications in Higher Order Logic
Abstract elided by the publisher.
An Action Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems
Abstract elided by the publisher.
An Overview and Synthesis on Timed Process Algebras
Abstract elided by the publisher.
Partial-Order Model Checking: A Guide for the Perplexed
Abstract elided by the publisher.
Error Diagnosis in Finite Communicating Systems
Abstract elided by the publisher.
Automating Most Parts of Hardware Proofs in HOL
Abstract elided by the publisher.
A Two-Level Formal Verification Methodology using HOL and COSMOS
Abstract elided by the publisher.
Automatic Temporal Verification of Buffer Systems
Abstract elided by the publisher.
Taming Infinite State Spaces
Abstract elided by the publisher.
Temporal Precondition Verification of Design Transformations
Abstract elided by the publisher.
Extension of the Karp and Miller Procedure to Lotos Specifications
Abstract elided by the publisher.
PAPETRI: Environment for the Analysis of Petri Nets
Abstract elided by the publisher.
Minimal Model Generation
Abstract elided by the publisher.
Formal Verification of Digital Circuits Using Symbolic Ternary System Models
Abstract elided by the publisher.
Verifying Liveness Properties by Verifying Safety Properties
Abstract elided by the publisher.
A Proof Lattice-Based Technique for Analyzing Liveness of Resource Controllers
Abstract elided by the publisher.
The Use of Model Checking in ATPG for Sequential Circuits
Abstract elided by the publisher.
Computer Assistance for Program Refinement
Abstract elided by the publisher.
Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem
Abstract elided by the publisher.