Algebraic_VCs
From MaRDI portal
Algebraic VCs
- A program construction and verification tool for separation logic
- Algebraic Notions of Termination
- Algebras of modal operators and partial correctness
- An equational axiomatization of dynamic negation and relational composition
- Automated Reasoning in Higher-Order Regular Algebra
- Building program construction and verification tools from algebraic principles
- Concrete semantics. With Isabelle/HOL
- Eisbach: a proof method language for Isabelle
- Forward with Hoare
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Internal axioms for domain semirings
- Isabelle/HOL. A proof assistant for higher-order logic
- Kleene algebra with domain
- Left omega algebras and regular equations
- Logical analysis of hybrid systems. Proving theorems for complex dynamics.
- On Hoare logic and Kleene algebra with tests
- On the expressive power of Kleene algebra with domain
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Refinement Calculus
Cited in
(9)- A discrete geometric model of concurrent program execution
- Ordinary Differential Equations
- Kleene Algebra
- Binary Multirelations
- KAD
- Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
- Quantales
- Transformer semantics
- Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
This page was built for software: Algebraic_VCs
