Building program construction and verification tools from algebraic principles
DOI10.1007/S00165-015-0343-1zbMATH Open1342.68066OpenAlexW2234482668MaRDI QIDQ736461FDOQ736461
Authors: Alasdair Armstrong, Victor B. F. Gomes, Georg Struth 
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
Recommendations
program verificationautomated theorem provinginteractive theorem provingformalised mathematicsalgebras of programsprogram constructionsemantics of imperative programs
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Dafny: an automatic program verifier for functional correctness
- Why3 -- where programs meet provers
- Isabelle/HOL. A proof assistant for higher-order logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Hoare type theory, polymorphism and separation
- Title not available (Why is that?)
- Automated Reasoning in Higher-Order Regular Algebra
- A program construction and verification tool for separation logic
- Automated Reasoning in Kleene Algebra
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Title not available (Why is that?)
- Kleene algebra with tests and Coq tools for while programs
- Algebras for program correctness in Isabelle/HOL
- On Hoare logic and Kleene algebra with tests
- Internal axioms for domain semirings
- Proof Pearl: regular expression equivalence and relation algebra
- An efficient Coq tactic for deciding Kleene algebras
- Algebras of modal operators and partial correctness
- A refinement strategy for Circus
- Verification of sequential and concurrent programs
- Hoare logic and auxiliary variables
- Winskel is (almost) right: Towards a mechanized semantics textbook
- Title not available (Why is that?)
- Relational Methods in Computer Science
- Imperative Functional Programming with Isabelle/HOL
- Certification of nontermination proofs
- Data refinement in Isabelle/HOL
- Program analysis and verification based on Kleene algebra in Isabelle/HOL
Cited In (21)
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
- The refinement calculus of reactive systems
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Calculational verification of reactive programs with reactive relations and Kleene algebra
- Unifying theories of reactive design contracts
- Hoare semigroups
- Title not available (Why is that?)
- Combining algebraic specifications and procedural tools for correct program development
- Relation-algebraic verification of disjoint-set forests
- On automated program construction and verification
- On the complexity of Kleene algebra with domain
- Kleene algebra with tests and Coq tools for while programs
- A program construction and verification tool for separation logic
- Program analysis and verification based on Kleene algebra in Isabelle/HOL
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- A discrete geometric model of concurrent program execution
- Towards interactive verification of programmable logic controllers using modal Kleene algebra and KIV
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- Unifying theories of time with generalised reactive processes
- Unifying heterogeneous state-spaces with lenses
- Algebraic implementations preserve program correctness
Uses Software
This page was built for publication: Building program construction and verification tools from algebraic principles
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q736461)
