Modal Kleene algebra applied to program correctness

DOI10.1007/978-3-319-48989-6_19MaRDI QIDQ2281640zbMATH OpenOpenAlexFDO

Authors Victor B. F. Gomes, Georg Struth

Publication date 3 January 2020

Full work available at URL https://www.repository.cam.ac.uk/handle/1810/260625

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Algebraic Methodology and Software Technology
• Application of modal logics to the specification and verification of programs
• scientific article; zbMATH DE number 3982508
• Kleene algebra and modal logic
• Automata-theoretic techniques for modal logics of programs
• Algebras for program correctness in Isabelle/HOL
• Algebras of modal operators and partial correctness
• scientific article; zbMATH DE number 3869303
• Program analysis and verification based on Kleene algebra in Isabelle/HOL
• Verifying hybrid systems with modal Kleene algebra

Cited in

(20)

• A relation algebraic model of robust correctness
• Verifying hybrid systems with modal Kleene algebra
• Kima: An automated error correction system for concurrent logic programs
• Unifying theories of reactive design contracts
• Automated verification of reactive and concurrent programs by calculation
• Cylindric Kleene lattices for program construction
• Specifying program properties using modal fixpoint logics: a survey of results
• Abstract strategies and coherence
• Towards interactive verification of programmable logic controllers using modal Kleene algebra and KIV
• Automated Reasoning in Kleene Algebra
• scientific article; zbMATH DE number 3921953 (Why is no real title available?)
• Automated Algebraic Reasoning for Collections and Local Variables with Lenses
• Algebraic Methodology and Software Technology
• Modal tools for separation and refinement
• Algebras for program correctness in Isabelle/HOL
• IsaVODEs: Interactive verification of cyber-physical systems at scale
• Modal quantales, involutive quantales, Dedekind Quantales
• Building program construction and verification tools from algebraic principles
• Algebras of modal operators and partial correctness
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL

Describes a project that uses

Uses Software

• HOL
• Isabelle
• Isabelle/HOL
• Eisbach

This page was built for publication: Modal Kleene algebra applied to program correctness

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2281640)