書誌事項
- 公開日
- 2016
- 資源種別
- journal article
- 権利情報
-
- http://www.springer.com/tdm
- DOI
-
- 10.1007/978-3-319-46520-3_20
- 公開者
- Springer International Publishing
この論文をさがす
説明
Kobayashi and Igarashi proposed model checking of \(\mu \)HORS (recursively-typed higher-order recursion schemes), by which a wide range of programs such as object-oriented programs and multi-threaded programs can be precisely modeled and verified. In this work, we present a procedure for \(\mu \)HORS model checking that improves the procedure based on automata-based abstraction refinement proposed by Kobayashi and Li. The new procedure optimizes each step of the abstract-check-refine paradigm of the previous procedure. Specially, it combines the strengths of automata-based and type-based abstraction refinement as equivalence-based abstraction refinement. We have implemented the new procedure, and confirmed that it always outperformed the original automata-based procedure on runtime efficiency, and successfully verified all benchmarks which were previously impossible.
収録刊行物
-
- Lecture Notes in Computer Science
-
Lecture Notes in Computer Science 304-320, 2016
Springer International Publishing
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1360848655498787200
-
- ISSN
- 16113349
- 03029743
-
- 資料種別
- journal article
-
- データソース種別
-
- Crossref
- KAKEN
- OpenAIRE
