Automatically disproving fair termination of higher-order functional programs

DOI10.1145/2951913.2951919zbMath1361.68153OpenAlexW2515762752MaRDI QIDQ2985774

Keiichi Watanabe, Takeshi Tsukada, Ryosuke Sato, 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 verificationpredicate abstractionhigher-order model checkingfair terminationCEGARhigher-order programs

Mathematics Subject Classification ID

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

Related Items (1)

Streett Automata Model Checking of Higher-Order Recursion Schemes

Uses Software

• z3
• HMC
• TravMC2
• HorSatP

This page was built for publication: Automatically disproving fair termination of higher-order functional programs