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

DOI10.1007/978-3-319-21668-3_17zbMATH Open1381.68035OpenAlexW1012186786MaRDI QIDQ1702897FDOQ1702897

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

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

Mathematics Subject Classification ID

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

Cited In (10)

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

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)