Automatically disproving fair termination of higher-order functional programs

DOI10.1145/2951913.2951919MaRDI QIDQ2985774zbMATH OpenOpenAlexFDO

Authors Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi

Publication date 10 May 2017

Published in Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2951913.2951919

zbMATH Keywords

automatic verificationCEGARfair terminationhigher-order model checkinghigher-order programspredicate abstraction

Mathematics Subject Classification ID

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

Recommendations

• Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
• Temporal verification of higher-order functional programs
• Automatic Termination Verification for Higher-Order Functional Programs
• Progress measures and stack assertions for fair termination
• Frontiers of Combining Systems

Cited in

(8)

• Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
• Temporal verification of higher-order functional programs
• A proof rule for fair termination of guarded commands
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Termination of Fair Computations in Term Rewriting
• Automatic Termination Verification for Higher-Order Functional Programs
• First order Büchi automata and their application to verification of LTL specifications
• Termination of just/fair computations in term rewriting

Describes a project that uses

Uses Software

• HMC
• TravMC2
• z3
• HorSatP

This page was built for publication: Automatically disproving fair 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 Q2985774)