Deciding KAT and Hoare logic with derivatives

zbMATH Open1459.68040arXiv1210.2456MaRDI QIDQ4986510FDOQ4986510

Nelma Moreira, Sabine Broda, Ricardo Almeida

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 (4)

• Title not available (Why is that?)
• KAT-ML: an interactive theorem prover for Kleene algebra with tests
• Deciding Synchronous Kleene Algebra with Derivatives
• Deciding Kleene algebra terms equivalence in Coq

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)