Deciding KAT and Hoare logic with derivatives

zbMATH Open1459.68040arXiv1210.2456MaRDI QIDQ4986510FDOQ4986510

Authors: Ricardo Almeida, Sabine Broda, Nelma Moreira 

Publication date: 27 April 2021

Full work available at URL: https://arxiv.org/abs/1210.2456

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

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)

Cited In (10)

• On Kleene algebras for weighted computation
• On the equivalence of automata for KAT-expressions
• Title not available (Why is that?)
• Deciding synchronous Kleene algebra with derivatives
• KAT-ML: an interactive theorem prover for Kleene algebra with tests
• Canonical finite models of 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)