Automated Reasoning in Kleene Algebra
From MaRDI portal
Publication:3608779
DOI10.1007/978-3-540-73595-3_19zbMath1184.68462MaRDI QIDQ3608779
Publication date: 6 March 2009
Published in: Automated Deduction – CADE-21 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-73595-3_19
68Q60: Specification and verification (program logics, model checking, etc.)
03G25: Other algebras related to logic
Related Items
Denotation by Transformation, A relation-algebraic approach to the ``Hoare logic of functional dependencies, Determination of \(\alpha \)-resolution in lattice-valued first-order logic \(\mathrm{LF}(X)\), Fixing Zeno gaps, Algebraic separation logic, Normal forms in total correctness for while programs and action systems, Algebraic notions of nontermination: Omega and divergence in idempotent semirings, Internal axioms for domain semirings, Dual choice and iteration in an abstract algebra of action, Normal design algebra, Enabledness and termination in refinement algebra, Algebraic neighbourhood logic, A sketch of a dynamic epistemic semiring, An algebra of hybrid systems, Automated verification of refinement laws, Dijkstra, Floyd and Warshall meet Kleene, Modal algebra and Petri nets, Extended transitive separation logic, Deciding Kleene algebra terms equivalence in Coq, Deciding Regular Expressions (In-)Equivalence in Coq, Automated Reasoning for Hybrid Systems — Two Case Studies —, Non-termination in Idempotent Semirings, Knowledge and Games in Modal Semirings, Circulations, Fuzzy Relations and Semirings, Modal Semirings Revisited
Uses Software
