Deciding KAT and Hoare logic with derivatives

MaRDI QIDQ4986510zbMATH OpenFDO

Authors Ricardo Almeida, Sabine Broda, Nelma Moreira

Publication date 27 April 2021

Full work available at URL https://arxiv.org/abs/1210.2456, http://eptcs.web.cse.unsw.edu.au/paper.cgi?GandALF2012.10

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70)

Recommendations

• On Hoare logic and Kleene algebra with tests
• On the equivalence of automata for KAT-expressions
• Canonical finite models of Kleene algebra with tests
• scientific article; zbMATH DE number 2090029
• A modified completeness theorem of KAT and decidability of term reducibility

Cited in

(10)

• On Kleene algebras for weighted computation
• On the equivalence of automata for KAT-expressions
• scientific article; zbMATH DE number 2090029 (Why is no real title available?)
• Deciding synchronous Kleene algebra with derivatives
• Canonical finite models of Kleene algebra with tests
• KAT-ML: an interactive theorem prover for Kleene algebra with tests
• A modified completeness theorem of KAT and decidability of term reducibility
• Program analysis and verification based on Kleene algebra in Isabelle/HOL
• Deciding Kleene algebra terms equivalence in Coq
• Local completeness logic on Kleene algebra with tests

This page was built for publication: Deciding KAT and Hoare logic with derivatives

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