Predicate abstraction and CEGAR for higher-order model checking
作者： Naoki Kobayashi , Ryosuke Sato , Hiroshi Unno
关键词: Model checking 、 Symbolic trajectory evaluation 、 Programming language 、 Recursion 、 Abstraction model checking 、 Predicate abstraction 、 Theoretical computer science 、 Computer science 、 Order (ring theory)
摘要: Higher-order model checking (more precisely, the of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties programs written in simply-typed λ-calculus with and finite data domains. This paper formalizes predicate abstraction counterexample-guided refinement (CEGAR) for checking, enabling automatic verification that use infinite domains such as integers. A prototype verifier functional based on formalization implemented tested several programs.
acm.org
elsevier.com
tsukuba.ac.jp 
sci-hub.se 参考文章(35)
Dirk Beyer, Damien Zufferey, Rupak Majumdar, CSIsat: Interpolation for LA+EUF computer aided verification. pp. 304- 308 ,(2008) , 10.1007/978-3-540-70545-1_29
Hiroshi Unno, Naoshi Tabuchi, Naoki Kobayashi, Verification of tree-processing programs via higher-order model checking asian symposium on programming languages and systems. pp. 312- 327 ,(2010) , 10.1007/978-3-642-17164-2_22
Susanne Graf, Hassen Saidi, Construction of Abstract State Graphs with PVS computer aided verification. pp. 72- 83 ,(1997) , 10.1007/3-540-63166-6_10
Ranjit Jhala, K. L. McMillan, A practical and complete approach to predicate refinement tools and algorithms for construction and analysis of systems. pp. 459- 473 ,(2006) , 10.1007/11691372_33
Naoki Kobayashi, A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes joint european conferences on theory and practice of software. pp. 260- 274 ,(2011) , 10.1007/978-3-642-19805-2_18
Andrey Rybalchenko, Ranjit Jhala, Rupak Majumdar, Refinement type inference via abstract interpretation pp. 1- 11 ,(2010)
Tachio Terauchi, Dependent types from counterexamples Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '10. ,vol. 45, pp. 119- 130 ,(2010) , 10.1145/1706299.1706315
Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno, Higher-order multi-parameter tree transducers and recursion schemes for program verification Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '10. ,vol. 45, pp. 495- 508 ,(2010) , 10.1145/1706299.1706355
Hongwei Xi, Frank Pfenning, Dependent types in practical programming Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '99. pp. 214- 227 ,(1999) , 10.1145/292540.292560
Werner Damm, The IO- and OI-hierarchies Theoretical Computer Science. ,vol. 20, pp. 95- 207 ,(1982) , 10.1016/0304-3975(82)90009-3