| dc.contributor | 資管系 | |
| dc.creator (作者) | 洪智鐸 | |
| dc.creator (作者) | Hong, Chih-Duo;Lin, Anthony Widjaja | |
| dc.date (日期) | 2024-01 | |
| dc.date.accessioned | 26-Mar-2024 16:16:42 (UTC+8) | - |
| dc.date.available | 26-Mar-2024 16:16:42 (UTC+8) | - |
| dc.date.issued (上傳時間) | 26-Mar-2024 16:16:42 (UTC+8) | - |
| dc.identifier.uri (URI) | https://nccur.lib.nccu.edu.tw/handle/140.119/150604 | - |
| dc.description.abstract (摘要) | Verifying safety and liveness over array systems is a highly challenging problem. Array systems naturally capture parameterized systems such as distributed protocols with an unbounded number of processes. Such distributed protocols often exploit process IDs during their computation, resulting in array systems whose element values range over an infinite domain. In this paper, we develop a new method for proving safety and liveness over array systems. The crux of the technique is to overapproximate an array system as a string rewriting system (i.e. over a finite alphabet) by means of a new predicate abstraction that exploits the so-called indexed predicates. This allows us to tap into powerful verification methods for string rewriting systems that have been heavily developed in the last few decades (e.g. regular model checking). We demonstrate how our method yields simple, automatically verifiable proofs of safety and liveness for challenging examples, including Dijkstra’s self-stabilizing protocol and the Chang-Roberts leader election. | |
| dc.format.extent | 171 bytes | - |
| dc.format.mimetype | text/html | - |
| dc.relation (關聯) | The 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024), IET London | |
| dc.title (題名) | Regular Abstractions for Array Systems | |
| dc.type (資料類型) | conference | |
