Predicate abstraction and CEGAR for disproving termination of higher-order functional programs

DOI10.1007/978-3-319-21668-3_17MaRDI QIDQ1702897zbMATH OpenOpenAlexFDO

Authors Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi

Publication date 1 March 2018

Full work available at URL https://doi.org/10.1007/978-3-319-21668-3_17

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Functional programming and lambda calculus (68N18)

Recommendations

• Automatically disproving fair termination of higher-order functional programs
• Automatic Termination Verification for Higher-Order Functional Programs
• Frontiers of Combining Systems
• Temporal verification of higher-order functional programs
• Termination analysis for partial functions

Cited in

(10)

• Sound and complete concolic testing for higher-order functions
• Constraint-based relational verification
• First order Büchi automata and their application to verification of LTL specifications
• An overview of the HFL model checking project
• Automatically disproving fair termination of higher-order functional programs
• Non-termination Checking for Imperative Programs
• On the termination problem for probabilistic higher-order recursive programs
• A Nonstandard Functional Programming Language
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking

Describes a project that uses

Uses Software

• MoCHi

This page was built for publication: Predicate abstraction and CEGAR for disproving termination of higher-order functional programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1702897)