1. NCCU Academic Hub
  2. 學術產出
  3. College of Commerce
  4. Periodical Articles
  5. Item

學術產出-Periodical Articles

Article View/Open

Publication Export

Google ScholarTM

政大圖書館

Citation Infomation

題名 Regular Abstractions for Array Systems
作者 洪智鐸
Hong, Chih-Duo;Lin, Anthony Widjaja
貢獻者 資管系
關鍵詞 Array theory; Regular model checking; In nite-state model checking; Abstract interpretation; Predicate abstraction; Distributed protocol veri cation
日期 2024-01
上傳時間 26-Mar-2024 15:24:07 (UTC+8)
摘要 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 novel framework for proving safety and liveness over array systems. The crux of the framework 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 two decades or so (e.g. regular model checking). We demonstrate how our method yields simple, automatically verifiable proofs of safety and liveness properties for challenging examples, including Dijkstra's self-stabilizing protocol and the Chang-Roberts leader election protocol.
關聯 Proceedings of the ACM on Programming Languages (PACMPL), Vol.8, No. POPL, pp.638-666
資料類型 article
DOI https://doi.org/10.1145/3632864
dc.contributor 資管系
dc.creator (作者) 洪智鐸
dc.creator (作者) Hong, Chih-Duo;Lin, Anthony Widjaja
dc.date (日期) 2024-01
dc.date.accessioned 26-Mar-2024 15:24:07 (UTC+8)-
dc.date.available 26-Mar-2024 15:24:07 (UTC+8)-
dc.date.issued (上傳時間) 26-Mar-2024 15:24:07 (UTC+8)-
dc.identifier.uri (URI) https://nccur.lib.nccu.edu.tw/handle/140.119/150568-
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 novel framework for proving safety and liveness over array systems. The crux of the framework 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 two decades or so (e.g. regular model checking). We demonstrate how our method yields simple, automatically verifiable proofs of safety and liveness properties for challenging examples, including Dijkstra's self-stabilizing protocol and the Chang-Roberts leader election protocol.
dc.format.extent 95 bytes-
dc.format.mimetype text/html-
dc.relation (關聯) Proceedings of the ACM on Programming Languages (PACMPL), Vol.8, No. POPL, pp.638-666
dc.subject (關鍵詞) Array theory; Regular model checking; In nite-state model checking; Abstract interpretation; Predicate abstraction; Distributed protocol veri cation
dc.title (題名) Regular Abstractions for Array Systems
dc.type (資料類型) article
dc.identifier.doi (DOI) 10.1145/3632864
dc.doi.uri (DOI) https://doi.org/10.1145/3632864