Event-based proof of the mutual exclusion property of Peterson's algorithm

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

zbMATH Keywords

verificationalgorithmparallel computingmathematical modeldistributed system

Mathematics Subject Classification ID

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

• Isabelle/HOL
• Mizar
• UNITY

Cites Work

• On interprocess communication. I: Basic formalism
• Modeling concurrency with partial orders
• Myths about the mutual exclusion problem
• Mizar: State-of-the-art and Beyond
• Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Event-based proof of the mutual exclusion property of Peterson's algorithm