Temporal verification of higher-order functional programs

DOI10.1145/2837614.2837667MaRDI QIDQ2828245zbMATH OpenOpenAlexFDO

Authors Akihiro Murase, Tachio Terauchi, Naoki Kobayashi, Hiroshi Unno, Ryosuke Sato

Publication date 24 October 2016

Published in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

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

zbMATH Keywords

temporal propertiesautomatic verificationCEGARautomata-theoretic verificationbinary reachability analysishigher-order programs

Mathematics Subject Classification ID

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

Recommendations

• Automatic Termination Verification for Higher-Order Functional Programs
• Automatically disproving fair termination of higher-order functional programs
• Automating relatively complete verification of higher-order functional programs
• Verifying higher-order functions with tree automata
• Model checking higher-order programs

Cited in

(10)

• A fixpoint logic and dependent effects for temporal property verification
• Temporal refinements for guarded recursive types
• Predicate abstraction and CEGAR for disproving termination of higher-order functional programs
• Automatically disproving fair termination of higher-order functional programs
• Verifying termination and reduction properties about higher-order logic programs
• A Nonstandard Functional Programming Language
• An overview of the HFL model checking project
• A temporal logic for higher-order functional programs
• Streett Automata Model Checking of Higher-Order Recursion Schemes
• Fold/unfold transformations for fixpoint logic

This page was built for publication: Temporal verification of higher-order functional programs

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