Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
From MaRDI portal
Publication:1702897
DOI10.1007/978-3-319-21668-3_17zbMath1381.68035OpenAlexW1012186786MaRDI QIDQ1702897
Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi, Takuya Kuwahara
Publication date: 1 March 2018
Full work available at URL: https://doi.org/10.1007/978-3-319-21668-3_17
Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (6)
Constraint-based relational verification ⋮ A Nonstandard Functional Programming Language ⋮ Sound and complete concolic testing for higher-order functions ⋮ Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking ⋮ Unnamed Item ⋮ Streett Automata Model Checking of Higher-Order Recursion Schemes
Uses Software
This page was built for publication: Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
