scientific article; zbMATH DE number 1086671
From MaRDI portal
Publication:4362921
zbMath0882.03064MaRDI QIDQ4362921
Publication date: 13 November 1997
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
completenessdecidabilityequational theoryKleene algebras with tests*-continuous Kleene algebraequational specification and verification
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Other algebras related to logic (03G25)
Related Items (73)
The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes ⋮ A Finite Axiomatisation of Finite-State Automata Using String Diagrams ⋮ Relations as Images ⋮ Stone Relation Algebras ⋮ Semantic Foundations for Deterministic Dataflow and Stream Processing ⋮ Canonical finite models of Kleene algebra with tests ⋮ Concurrent Kleene algebra with tests and branching automata ⋮ Algebraic Semantics for Dynamic Dynamic Logic ⋮ Computable execution traces ⋮ Concurrent Kleene Algebra ⋮ Transitive Separation Logic ⋮ Unifying Lazy and Strict Computations ⋮ Deciding Regular Expressions (In-)Equivalence in Coq ⋮ Generalised rely-guarantee concurrency: an algebraic foundation ⋮ A Relation-Algebraic Approach to Multirelations and Predicate Transformers ⋮ A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency ⋮ Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras ⋮ A Hierarchy of Algebras for Boolean Subsets ⋮ Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL ⋮ Latest News about Demonic Algebra with Domain ⋮ Automatic Proof Generation in Kleene Algebra ⋮ Efficiently Deciding μ-Calculus with Converse over Finite Trees ⋮ Internal axioms for domain semirings ⋮ Dijkstra, Floyd and Warshall meet Kleene ⋮ Embedding Kozen-Tiuryn logic into residuated one-sorted Kleene algebra with tests ⋮ Lifting numeric relational domains to algebraic data types ⋮ Deciding program properties via complete abstractions on bounded domains ⋮ Local completeness logic on Kleene algebra with tests ⋮ Unnamed Item ⋮ Completeness and the finite model property for Kleene algebra, reconsidered ⋮ On the complexity of Kleene algebra with domain ⋮ Practical coinduction ⋮ On the expressive power of Kleene algebra with domain ⋮ Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems ⋮ Words-to-Letters Valuations for Language Kleene Algebras with Variable Complements ⋮ On tools for completeness of Kleene algebra with hypotheses ⋮ Free Kleene algebras with domain ⋮ Enabledness and termination in refinement algebra ⋮ Equational Theories of Abnormal Termination Based on Kleene Algebra ⋮ Local variable scoping and Kleene algebra with tests ⋮ Using probabilistic Kleene algebra pKA for protocol verification ⋮ Infinitary action logic: complexity, models and grammars ⋮ Algebraic foundations for qualitative calculi and networks ⋮ On the Coalgebraic Theory of Kleene Algebra with Tests ⋮ Algebraic reasoning for probabilistic action systems and while-loops ⋮ A string diagrammatic axiomatisation of finite-state automata ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ Algebra-coalgebra duality in brzozowski's minimization algorithm ⋮ What’s Decidable About Program Verification Modulo Axioms? ⋮ On the expressiveness of single-pass instruction sequences ⋮ Dual choice and iteration in an abstract algebra of action ⋮ A coalgebraic approach to Kleene algebra with tests ⋮ A Formal Language for Electronic Contracts ⋮ Refinement algebra for probabilistic programs ⋮ Algebras for iteration and infinite computations ⋮ Verification of Common Interprocedural Compiler Optimizations Using Visibly Pushdown Kleene Algebra ⋮ An algebra of hybrid systems ⋮ Probabilistic NetKAT ⋮ Building program construction and verification tools from algebraic principles ⋮ Partial Derivative Automata Formalized in Coq ⋮ Operational semantics with semicommutations ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Algebraic properties of if-then-else and commutative three-valued tests ⋮ Clausal Tableaux for Hybrid PDL ⋮ Algebra of Monotonic Boolean Transformers ⋮ Equational theories for automata ⋮ Undecidable Problems for Probabilistic Network Programming ⋮ Reversible Kleene lattices ⋮ On the relation between concurrent separation logic and concurrent Kleene algebra ⋮ Deciding Kleene algebra terms equivalence in Coq ⋮ A goal-directed decision procedure for hybrid PDL
This page was built for publication:
