Event-based proof of the mutual exclusion property of Peterson's algorithm
From MaRDI portal
Publication:271900
DOI10.1515/FORMA-2015-0026zbMath1334.68030OpenAlexW2313864317MaRDI QIDQ271900
Mykola Nikitchenko, Ievgen Ivanov, Uri Abraham
Publication date: 20 April 2016
Published in: Formalized Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1515/forma-2015-0026
Mechanization of proofs and logical operations (03B35) Distributed systems (68M14) Distributed algorithms (68W15)
Related Items (5)
Composition-nominative logics as institutions ⋮ Simple-named complex-valued nominative data -- definition and basic operations ⋮ Kleene algebra of partial predicates ⋮ On algebras of algorithms and specifications over uninterpreted data ⋮ On an algorithmic algebra over simple-named complex-valued nominative data
Uses Software
Cites Work
This page was built for publication: Event-based proof of the mutual exclusion property of Peterson's algorithm