Automated verification of refinement laws

DOI10.1007/S10472-009-9151-8MaRDI QIDQ1037397zbMATH OpenOpenAlexFDO

Authors Peter Höfner, Georg Struth, Geoff Sutcliffe

Publication date 16 November 2009

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL http://eprints.whiterose.ac.uk/10049/1/Struth1.pdf

zbMATH Keywords

Kleene algebrasdemonic refinement algebras

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other algebras related to logic (03G25)

Recommendations

• Towards a refinement algebra
• Algebras for program correctness in Isabelle/HOL
• scientific article; zbMATH DE number 2090029
• Mechanizing some advanced refinement concepts
• Abstract representation theorems for demonic refinement algebras

Cites work

• scientific article; zbMATH DE number 1722713 (Why is no real title available?)
• scientific article; zbMATH DE number 1809860 (Why is no real title available?)
• scientific article; zbMATH DE number 1809861 (Why is no real title available?)
• scientific article; zbMATH DE number 1809862 (Why is no real title available?)
• scientific article; zbMATH DE number 5305114 (Why is no real title available?)
• scientific article; zbMATH DE number 2090029 (Why is no real title available?)
• A completeness theorem for Kleene algebras and the algebra of regular events
• Abstract abstract reduction
• Automated Reasoning for Hybrid Systems — Two Case Studies —
• Automated Reasoning in Kleene Algebra
• Certification of Automated Termination Proofs
• Data Refinement
• Domain Axioms for a Family of Near-Semirings
• Evaluating general purpose automated theorem proving systems
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• IeanCOP: lean connection-based theorem proving
• Modal Semirings Revisited
• Modal tools for separation and refinement
• On Automating the Calculus of Relations
• Ordered chaining calculi for first-order theories of transitive relations
• Reasoning algebraically about loops
• SRASS - A Semantic Relevance Axiom Selection System
• System Description: Spass Version 3.0
• The TPTP problem library. CNF release v1. 2. 1
• The state of CASC
• Towards a refinement algebra
• Transition invariants and transition predicate abstraction for program termination
• Using probabilistic Kleene algebra pKA for protocol verification

Cited in

(5)

• Internal axioms for domain semirings
• Dual choice and iteration in an abstract algebra of action
• Automatic verification of differential characteristics: application to reduced Gimli
• Algebraic separation logic
• An algebraic approach to computations with progress

Describes a project that uses

Uses Software

• OTTER
• VAMPIRE
• SPASS
• TPTP
• Metis
• Prover9
• Mace4
• E Theorem Prover
• MaLARea
• SRASS
• FLOTTER

This page was built for publication: Automated verification of refinement laws

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1037397)