Automated verification of refinement laws
type: Item
instance of: scholarly article
title: Automated verification of refinement laws
zbMATH Open document ID: 1184.68463
author: Peter Höfner
author: Georg Struth
author: Geoff Sutcliffe
published in: Annals of Mathematics and Artificial Intelligence
publication date: 2009-11-16T00:00:00Z
full work available at URL: Struth1.pdf
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03G25
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 5633343
zbMATH Keywords: demonic refinement algebras
zbMATH Keywords: Kleene algebras
describes a project that uses: VAMPIRE
describes a project that uses: Mace4
describes a project that uses: Metis_
describes a project that uses: SPASS
describes a project that uses: TPTP
describes a project that uses: E Theorem Prover
describes a project that uses: MaLARea
describes a project that uses: OTTER
describes a project that uses: Prover9
describes a project that uses: SRASS
describes a project that uses: FLOTTER
MaRDI profile type: Publication
OpenAlex ID: W2026501147
cites work: Ordered chaining calculi for first-order theories of transitive relations
cites work: Reasoning algebraically about loops
cites work: Certification of Automated Termination Proofs
cites work: Geometric Resolution: A Proof Procedure Based on Finite Model Search
cites work: Data Refinement
cites work: Domain Axioms for a Family of Near-Semirings
cites work: Modal Semirings Revisited
cites work: Automated Reasoning for Hybrid Systems — Two Case Studies —
cites work: Automated Reasoning in Kleene Algebra
cites work: On Automating the Calculus of Relations
cites work: A completeness theorem for Kleene algebras and the algebra of regular events
cites work: Using probabilistic Kleene algebra pKA for protocol verification
cites work: IeanCOP: lean connection-based theorem proving
cites work: Q3150299
cites work: Transition Invariants and Transition Predicate Abstraction for Program Termination
cites work: Q3150300
cites work: Q3150301
cites work: Q2778885
cites work: Abstract abstract reduction
cites work: Modal Tools for Separation and Refinement
cites work: Q3515519
cites work: SRASS - A Semantic Relevance Axiom Selection System
cites work: Q5486135
cites work: The TPTP problem library. CNF release v1. 2. 1
cites work: Evaluating general purpose automated theorem proving systems
cites work: Q4808696
cites work: Towards a refinement algebra
cites work: System Description: Spass Version 3.0
DOI: 10.1007/S10472-009-9151-8
description: scientific article; zbMATH DE number 5633343