Liveness Reasoning with Isabelle/HOL

DOI10.1007/978-3-642-03359-9_33zbMath1252.68198OpenAlexW1485043971MaRDI QIDQ3183549

Jinshuang Wang, Huabing Yang, Xing-Yuan Zhang

Publication date: 20 October 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_33

zbMATH Keywords

probabilistic modelinductive protocol verificationliveness proofparametric fairness

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (1)

Priority inheritance protocol proved correct

Uses Software

• Isabelle
• Isabelle/HOL
• Isar

Cites Work

• Unnamed Item
• On fairness and randomness
• Completing the temporal picture
• Isabelle/HOL. A proof assistant for higher-order logic
• Probabilistic verification
• On the verification of qualitative properties of probabilistic processes under fairness constraints.
• Theorem Proving in Higher Order Logics

This page was built for publication: Liveness Reasoning with Isabelle/HOL