Automatic Termination Verification for Higher-Order Functional Programs
作者： Takuya Kuwahara , Tachio Terauchi , Hiroshi Unno , Naoki Kobayashi
DOI: 10.1007/978-3-642-54833-8_21
关键词: Inference 、 Soundness 、 Closure (mathematics) 、 Program transformation 、 Computer science 、 Completeness (order theory) 、 Call graph 、 Reachability 、 Ranking 、 Theoretical computer science 、 Programming language
摘要: We present an automated approach to verifying termination of higher-order functional programs. Our adopts the idea from recent work on verification via transition invariants a.k.a.i¾?binary reachability analysis, and is fully automated. able soundly handle subtle aspects programs, including partial applications, indirect calls, ranking functions over function closure values. In contrast previous approaches for our sound complete, relative soundness completeness underlying analysis inference. have implemented a prototype subset OCaml language, we confirmed that it automatically verify some non-trivial
springer.com
elsevier.com
tsukuba.ac.jp 
researchgate.net 
sqlab.jp 参考文章(52)
He Zhu, Suresh Jagannathan, Compositional and Lightweight Dependent Type Inference for ML verification model checking and abstract interpretation. pp. 295- 314 ,(2013) , 10.1007/978-3-642-35873-9_19
Robin Neatherway, Steven Ramsay, Model checking liveness properties of higher-order functional programs ,(2010)
K. Etessami, Analysis of Recursive Game Graphs Using Data Flow Equations verification model checking and abstract interpretation. pp. 282- 296 ,(2004) , 10.1007/978-3-540-24622-0_23
Leonardo de Moura, Nikolaj Bjørner, Z3: an efficient SMT solver tools and algorithms for construction and analysis of systems. pp. 337- 340 ,(2008) , 10.1007/978-3-540-78800-3_24
Byron Cook, Andreas Podelski, Andrey Rybalchenko, Abstraction Refinement for Termination Static Analysis. pp. 87- 101 ,(2005) , 10.1007/11547662_8
Jürgen Giesl, René Thiemann, Peter Schneider-Kamp, Stephan Falke, Automated Termination Proofs with AProVE Rewriting Techniques and Applications. pp. 210- 220 ,(2004) , 10.1007/978-3-540-25979-4_15
Andreas Podelski, Andrey Rybalchenko, A Complete Method for the Synthesis of Linear Ranking Functions verification model checking and abstract interpretation. pp. 239- 251 ,(2004) , 10.1007/978-3-540-24622-0_20
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
Byron Cook, Abigail See, Florian Zuleger, Ramsey vs. lexicographic termination proving tools and algorithms for construction and analysis of systems. pp. 47- 61 ,(2013) , 10.1007/978-3-642-36742-7_4
Matthias Heizmann, Neil D. Jones, Andreas Podelski, Size-change termination and transition invariants static analysis symposium. pp. 22- 50 ,(2010) , 10.1007/978-3-642-15769-1_4