Formal Verification of Concurrent Algorithms: Case Studies on Mutual Exclusion.
2023 IEEE 28th Pacific Rim International Symposium on Dependable Computing (PRDC)(2023)
摘要
Concurrent algorithms are difficult to design correctly. This study focused on mutual exclusion and explored the benefits of employing a formal approach for specifying and verifying concurrent algorithms through case studies. This paper reports the findings and insight obtained from the case studies, including the detection of a design fault in one of the analyzed algorithms.
更多查看译文
关键词
Model checking,mutual exclusion,TLA,Plus-CAL,formal specification
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要