Email Gateway (Aug 22 2022 at 13:38): Email Gateway (Aug 22 2022 at 13:38):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
A new entry is available in the AFP:
Program Construction and Verification Components Based on Kleene Algebra
by Victor B. F. Gomes and Georg Struth
Variants of Kleene algebra support program construction and verification by algebraic reasoning. This entry provides a verification component for Hoare logic based on Kleene algebra with tests, verification components for weakest preconditions and strongest postconditions based on Kleene algebra with domain and a component for step-wise refinement based on refinement Kleene algebra with tests. In addition to these components for the partial correctness of while programs, a verification component for total correctness based on divergence Kleene algebras and one for (partial correctness) of recursive programs based on domain quantales are provided. Finally we have integrated memory models for programs with pointers and a program trace semantics into the weakest precondition component.
http://www.isa-afp.org/entries/Algebraic_VCs.shtml
Enjoy!
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 27 2024 at 01:05 UTC