Building program construction and verification tools from algebraic principles

DOI10.1007/s00165-015-0343-1zbMath1342.68066OpenAlexW2234482668MaRDI QIDQ736461

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

Publication date: 4 August 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-015-0343-1

zbMATH Keywords

automated theorem provingprogram verificationinteractive theorem provingformalised mathematicsalgebras of programsprogram constructionsemantics of imperative programs

Mathematics Subject Classification ID

Related Items (10)

Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ The refinement calculus of reactive systems ⋮ Automated Algebraic Reasoning for Collections and Local Variables with Lenses ⋮ Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL ⋮ On the complexity of Kleene algebra with domain ⋮ A Discrete Geometric Model of Concurrent Program Execution ⋮ Unifying theories of time with generalised reactive processes ⋮ Hoare Semigroups ⋮ Unifying theories of reactive design contracts

Uses Software

• Coq
• Dafny
• Isabelle/HOL
• Why3
• WhyML
• Circus
• Archive Formal Proofs
• Regular Sets
• Kleene Algebra
• Simpl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Programming and automating mathematics in the Tarski-Kleene hierarchy
• Internal axioms for domain semirings
• A refinement strategy for Circus
• Algebras of modal operators and partial correctness
• Verification of sequential and concurrent programs
• Winskel is (almost) right: Towards a mechanized semantics textbook
• Isabelle/HOL. A proof assistant for higher-order logic
• Hoare logic and auxiliary variables
• Proof Pearl: regular expression equivalence and relation algebra
• Certification of Nontermination Proofs
• Automated Reasoning in Higher-Order Regular Algebra
• A Program Construction and Verification Tool for Separation Logic
• Dafny: An Automatic Program Verifier for Functional Correctness
• Imperative Functional Programming with Isabelle/HOL
• Hoare type theory, polymorphism and separation
• Automated Reasoning in Kleene Algebra
• Why3 — Where Programs Meet Provers
• Data Refinement in Isabelle/HOL
• Kleene Algebra with Tests and Coq Tools for while Programs
• Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
• Algebras for Program Correctness in Isabelle/HOL
• On Hoare logic and Kleene algebra with tests
• An Efficient Coq Tactic for Deciding Kleene Algebras
• Relational Methods in Computer Science

This page was built for publication: Building program construction and verification tools from algebraic principles