Peterson’s algorithm Total correctness proof in IPCL

• Опубліковано в: PROBLEMS IN PROGRAMMING
• Дата: 2018
• Випуск: 2-3
• Сторінки: 113-118
• ISSN: 1727-4907
• Автори та афіліації: A.A. Zhygallo — Kiev Taras Shevchkenko National University
• Автор: Zhygallo, A.A.
• Формат: Стаття
• Мова: Англійська
• Опубліковано: PROBLEMS IN PROGRAMMING 2018
• Теми: Peterson’s algorithm; mutual exclusion; software total correctness; formal verification; liveness property; concurrent program; interleaving; IPCL; composition-nominative languages; UDC 004.415.52
• Онлайн доступ: https://pp.isofts.kiev.ua/index.php/ojs1/article/view/186
• Назва журналу: Problems in programming

The total correctness of the Peterson’s Algorithm has been proved. States and transitions were fixed by the program. Runtime environment considered is interleaving concurrency with shared memory. Invariant of the program was constructed. All reasoning provided in terms of Method for software propert...