Formal Modeling and Verification of Lycklama and Hadzilacos’s Mutual Exclusion Algorithm

This study describes our thorough experience of formal modeling and exhaustive verification of concurrent systems, particularly mutual exclusion algorithms. The experience focuses on Lycklama and Hadzilacos’s (LH) mutual exclusion algorithm. LH rests on the reduced size of the shared state, contains...

وصف كامل

التفاصيل البيبلوغرافية

المؤلف الرئيسي:	Libero Nigro
التنسيق:	Artigo
اللغة:	Inglês
منشور في:	MDPI AG 2024-08-01
سلاسل:	Mathematics
الموضوعات:	concurrency/parallelism mutual exclusion algorithms properties atomic and non-atomic memory models formal modelling exhaustive model checking
الوصول للمادة أونلاين:	https://www.mdpi.com/2227-7390/12/16/2443
الوسوم:	إضافة وسم لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!