scientific article; zbMATH DE number 734956

Publication date: 19 March 1995

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

communication protocols computer-aided verification Boolean algebra homomorphisms cache coherency protocols language homomorphisms telephone switches

Mathematics Subject Classification ID

Computer science aspects of computer-aided design (68U07) Algebraic theory of languages and automata (68Q70) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Natural language processing (68T50)

Related Items (55)

Abstraction and composition: a verification method for co-operating systems ⋮ Infinite-state invariant checking with IC3 and predicate abstraction ⋮ Weighted automata and weighted logics ⋮ Weighted automata and weighted logics with discounting ⋮ Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning ⋮ An iterative approach to verification of real-time systems ⋮ Introduction to Model Checking ⋮ Automata Theory and Model Checking ⋮ SAT-Based Model Checking ⋮ Transfer of Model Checking to Industrial Practice ⋮ Weighted automata and weighted logics on infinite words ⋮ GSTE is partitioned model checking ⋮ Refinement preserving approximations for the design and verification of heterogeneous systems ⋮ A transformation-based approach to implication of GSTE assertion graphs ⋮ Model checking with fairness assumptions using PAT ⋮ Approximating Behaviors in Embedded System Design ⋮ Mechanizing the Powerset Construction for Restricted Classes of ω-Automata ⋮ A methodology to take credit for high-level verification during RTL verification ⋮ The Birth of Model Checking ⋮ A model checking-based approach for security policy verification of mobile systems ⋮ An automatic method for the dynamic construction of abstractions of states of a formal model ⋮ Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems ⋮ Verification of evolving software via component substitutability analysis ⋮ Automatic symbolic compositional verification by learning assumptions ⋮ Certifying inexpressibility ⋮ Verification of Boolean programs with unbounded thread creation ⋮ An automatic abstraction technique for verifying featured, parameterised systems ⋮ The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ The Quest for a Tight Translation of Büchi to co-Büchi Automata ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ Abstractions of data types ⋮ Verification by augmented abstraction: The automata-theoretic view ⋮ Proving the Refuted: Symbolic Model Checkers as Proof Generators ⋮ Meanings of Model Checking ⋮ Abstract reduction in directed model checking CCS processes ⋮ Safe Reasoning with Logic LTS ⋮ Complexity and Algorithms for Monomial and Clausal Predicate Abstraction ⋮ From Philosophical to Industrial Logics ⋮ An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps ⋮ Model checking with strong fairness ⋮ Compositional SCC analysis for language emptiness ⋮ Automata-Theoretic Model Checking Revisited ⋮ Survey on Directed Model Checking ⋮ Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata ⋮ Efficient Automatic STE Refinement Using Responsibility ⋮ Abstract Counterexamples for Non-disjunctive Abstractions ⋮ CONTROLLABILITY AND COOPERATIVENESS ANALYSIS FOR AUTOMATIC ABSTRACTION REFINEMENT ⋮ BÜCHI COMPLEMENTATION MADE TIGHTER ⋮ TYPENESS FOR ω-REGULAR AUTOMATA ⋮ A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas ⋮ Specification and Verification using Message Sequence Charts ⋮ A Logical Process Calculus ⋮ On the complexity of verifying concurrent transition systems ⋮ Automated analysis of fault-tolerance in distributed systems

Uses Software

This page was built for publication: