Automated verification of refinement laws

DOI10.1007/S10472-009-9151-8zbMATH Open1184.68463OpenAlexW2026501147MaRDI QIDQ1037397FDOQ1037397

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

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

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)

Cites Work

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

Cited In (5)

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

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)