Algebras for program correctness in Isabelle/HOL

DOI10.1007/978-3-319-06251-8_4MaRDI QIDQ5410477zbMATH OpenOpenAlexFDO

Authors Alasdair Armstrong, Victor B. F. Gomes, Georg Struth

Publication date 16 April 2014

Published in Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-06251-8_4

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Algebraic theory of languages and automata (68Q70)

Recommendations

• Program analysis and verification based on Kleene algebra in Isabelle/HOL
• Towards a refinement algebra
• scientific article; zbMATH DE number 2090029
• Modal Kleene algebra applied to program correctness
• scientific article; zbMATH DE number 2110621

Cited in

(17)

• Automated verification of refinement laws
• Algebraic implementations preserve program correctness
• Modal Kleene algebra applied to program correctness
• A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency
• Developments in concurrent Kleene algebra
• A while program normal form theorem in total correctness
• scientific article; zbMATH DE number 3986619 (Why is no real title available?)
• scientific article; zbMATH DE number 2090029 (Why is no real title available?)
• Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
• Kleene algebra with tests and Coq tools for while programs
• Program analysis and verification based on Kleene algebra in Isabelle/HOL
• Normal forms in total correctness for while programs and action systems
• Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
• Specifying and reasoning about shared-variable concurrency
• A Coq implementation of the program algebra in Jifeng He's new roadmap for linking theories of programming
• Building program construction and verification tools from algebraic principles
• Algebras of modal operators and partial correctness

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

This page was built for publication: Algebras for program correctness in Isabelle/HOL

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