Using partial orders for the efficient verification of deadlock freedom and safety properties |
| |
Authors: | Patrice Godefroid Pierre Wolper |
| |
Affiliation: | (1) Institut Montefiore, B28, Université de Liège, 4000 Liège Sart-Tilman, Belgium |
| |
Abstract: | This article presents an algorithm for detecting deadlocks in concurrent finite-state systems without incurring most of the state explosion due to the modeling of concurrency by interleaving. For systems that have a high level of concurrency, our algorithm can be much more efficient than the classical exploration of the whole state space. Finally, we show that our algorithm can also be used for verifying arbitrary safety properties. |
| |
Keywords: | verification concurrent programming state-space exploration deadlock detection state-space explosion |
本文献已被 SpringerLink 等数据库收录! |