Temporal verification of higher-order functional programs

DOI10.1145/2837614.2837667zbMath1347.68233OpenAlexW2294349880MaRDI QIDQ2828245

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

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

automatic verificationtemporal propertiesCEGARautomata-theoretic verificationbinary reachability analysishigher-order programs

Mathematics Subject Classification ID

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

Related Items

A Nonstandard Functional Programming Language, Temporal refinements for guarded recursive types, Fold/Unfold Transformations for Fixpoint Logic, Streett Automata Model Checking of Higher-Order Recursion Schemes