Building program construction and verification tools from algebraic principles
type: Item
instance of: scholarly article
title: Building program construction and verification tools from algebraic principles
zbMATH Open document ID: 1342.68066
author: Alasdair Armstrong
author: Victor B. F. Gomes
author: Georg Struth
published in: Formal Aspects of Computing
publication date: 2016-08-04T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6609071
zbMATH Keywords: program construction
zbMATH Keywords: program verification
zbMATH Keywords: semantics of imperative programs
zbMATH Keywords: algebras of programs
zbMATH Keywords: formalised mathematics
zbMATH Keywords: interactive theorem proving
zbMATH Keywords: automated theorem proving
describes a project that uses: Dafny
describes a project that uses: Why3
describes a project that uses: Archive Formal Proofs
describes a project that uses: Simpl
describes a project that uses: Kleene Algebra
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: WhyML
describes a project that uses: Circus
describes a project that uses: Regular Sets
MaRDI profile type: Publication
full work available at URL: s00165-015-0343-1
OpenAlex ID: W2234482668
cites work: Proof Pearl: regular expression equivalence and relation algebra
cites work: Verification of sequential and concurrent programs
cites work: Internal axioms for domain semirings
cites work: Algebras for Program Correctness in Isabelle/HOL
cites work: A refinement strategy for Circus
cites work: On Hoare logic and Kleene algebra with tests
cites work: Programming and automating mathematics in the Tarski-Kleene hierarchy
cites work: Automated Reasoning in Higher-Order Regular Algebra
cites work: Winskel is (almost) right: Towards a mechanized semantics textbook
cites work: Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
cites work: Imperative Functional Programming with Isabelle/HOL
cites work: An Efficient Coq Tactic for Deciding Kleene Algebras
cites work: A Program Construction and Verification Tool for Separation Logic
cites work: Why3 — Where Programs Meet Provers
cites work: Data Refinement in Isabelle/HOL
cites work: Automated Reasoning in Kleene Algebra
cites work: Hoare logic and auxiliary variables
cites work: Q4362921
cites work: Q2767087
cites work: Dafny: An Automatic Program Verifier for Functional Correctness
cites work: Q4301161
cites work: Algebras of modal operators and partial correctness
cites work: Relational Methods in Computer Science
cites work: Q4411818
cites work: Hoare type theory, polymorphism and separation
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Kleene Algebra with Tests and Coq Tools for while Programs
cites work: Certification of Nontermination Proofs
cites work: Q3969890
DOI: 10.1007/S00165-015-0343-1
description: scientific article; zbMATH DE number 6609071