Building program construction and verification tools from algebraic principles
From MaRDI portal
Recommendations
Cites work
- A program construction and verification tool for separation logic
- A refinement strategy for Circus
- Algebras for program correctness in Isabelle/HOL
- Algebras of modal operators and partial correctness
- An efficient Coq tactic for deciding Kleene algebras
- Automated Reasoning in Higher-Order Regular Algebra
- Automated Reasoning in Kleene Algebra
- Certification of nontermination proofs
- Dafny: an automatic program verifier for functional correctness
- Data refinement in Isabelle/HOL
- Hoare logic and auxiliary variables
- Hoare type theory, polymorphism and separation
- scientific article; zbMATH DE number 1696821 (Why is no real title available?)
- scientific article; zbMATH DE number 3793435 (Why is no real title available?)
- scientific article; zbMATH DE number 605806 (Why is no real title available?)
- scientific article; zbMATH DE number 1086671 (Why is no real title available?)
- scientific article; zbMATH DE number 1948157 (Why is no real title available?)
- Imperative Functional Programming with Isabelle/HOL
- Internal axioms for domain semirings
- Isabelle/HOL. A proof assistant for higher-order logic
- Kleene algebra with tests and Coq tools for while programs
- On Hoare logic and Kleene algebra with tests
- Program analysis and verification based on Kleene algebra in Isabelle/HOL
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Proof Pearl: regular expression equivalence and relation algebra
- Relational Methods in Computer Science
- Verification of sequential and concurrent programs
- Why3 -- where programs meet provers
- Winskel is (almost) right: Towards a mechanized semantics textbook
Cited in
(31)- Algebraic implementations preserve program correctness
- Generating algebraic laws from imperative programs
- Calculational verification of reactive programs with reactive relations and Kleene algebra
- Unifying theories of time with generalised reactive processes
- Unifying theories of reactive design contracts
- The refinement calculus of reactive systems
- A program construction and verification tool for separation logic
- A discrete geometric model of concurrent program execution
- Unifying heterogeneous state-spaces with lenses
- scientific article; zbMATH DE number 3872646 (Why is no real title available?)
- Towards interactive verification of programmable logic controllers using modal Kleene algebra and KIV
- On automated program construction and verification
- Algebraic_VCs
- Hoare semigroups
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- Kleene algebra with tests and Coq tools for while programs
- Program analysis and verification based on Kleene algebra in Isabelle/HOL
- Combining algebraic specifications and procedural tools for correct program development
- Transformer semantics
- On the complexity of Kleene algebra with domain
- Relation-algebraic verification of disjoint-set forests
- IsaVODEs: Interactive verification of cyber-physical systems at scale
- Modal algebra of multirelations
- Verification Components for Hybrid Systems
- Matrices for ODEs
- Optics
- Shallow Expressions
- Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
- Z Mathematical Toolkit in Isabelle/HOL
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
Describes a project that uses
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)
