Using probabilistic Kleene algebra pKA for protocol verification
From MaRDI portal
Publication:929968
DOI10.1016/j.jlap.2007.10.005zbMath1148.68034OpenAlexW2034320901WikidataQ114851556 ScholiaQ114851556MaRDI QIDQ929968
Publication date: 19 June 2008
Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlap.2007.10.005
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Distributed systems (68M14) Network protocols (68M12)
Related Items
Layered reasoning for randomized distributed algorithms, Compositional refinement in agent-based security protocols, Using probabilistic Kleene algebra pKA for protocol verification, Probabilistic NetKAT, Preface, Automated verification of refinement laws, Domain Axioms for a Family of Near-Semirings, A semantics and a logic for \textit{Fuzzy Arden Syntax}
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Using probabilistic Kleene algebra pKA for protocol verification
- N-process mutual exclusion with bounded waiting by 4. log//2N-valued shared variable
- Probabilistic models for the guarded command language
- Probabilistic guarded commands mechanized in HOL
- The Shadow Knows: Refinement of Ignorance in Sequential Programs
- KAT-ML: an interactive theorem prover for Kleene algebra with tests
- Reasoning with time and chance
- Knowledge, probability, and adversaries
- Refinement Calculus
- Abstraction, Refinement and Proof for Probabilistic Systems
- Mathematics of Program Construction
- Proving probabilistic correctness statements
- Randomized mutual exclusion algorithms revisited
- Formal verification of timed properties of randomized distributed algorithms
- Towards Automated Proof Support for Probabilistic Distributed Systems
- Monodic Tree Kleene Algebra
- A Proof-Theoretic Approach to Tactics
