Automated verification of refinement laws
From MaRDI portal
Publication:1037397
DOI10.1007/s10472-009-9151-8zbMath1184.68463OpenAlexW2026501147MaRDI QIDQ1037397
Geoff Sutcliffe, Georg Struth, Peter Höfner
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
Specification and verification (program logics, model checking, etc.) (68Q60) Other algebras related to logic (03G25)
Related Items
An algebraic approach to computations with progress ⋮ Internal axioms for domain semirings ⋮ Dual choice and iteration in an abstract algebra of action ⋮ Algebraic separation logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Abstract abstract reduction
- Using probabilistic Kleene algebra pKA for protocol verification
- The TPTP problem library. CNF release v1. 2. 1
- Reasoning algebraically about loops
- A completeness theorem for Kleene algebras and the algebra of regular events
- IeanCOP: lean connection-based theorem proving
- Evaluating general purpose automated theorem proving systems
- Towards a refinement algebra
- Transition Invariants and Transition Predicate Abstraction for Program Termination
- Ordered chaining calculi for first-order theories of transitive relations
- Automated Reasoning for Hybrid Systems — Two Case Studies —
- Modal Semirings Revisited
- Certification of Automated Termination Proofs
- On Automating the Calculus of Relations
- Automated Reasoning in Kleene Algebra
- SRASS - A Semantic Relevance Axiom Selection System
- System Description: Spass Version 3.0
- Geometric Resolution: A Proof Procedure Based on Finite Model Search
- Data Refinement
- Modal Tools for Separation and Refinement
- Domain Axioms for a Family of Near-Semirings
