Temporal verification of higher-order functional programs

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

Abstract

We present an automated approach to verifying arbitrary omegaregular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the "calling relation" is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.

Original languageEnglish
Title of host publicationPOPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PublisherAssociation for Computing Machinery
Pages57-68
Number of pages12
Volume20-22-January-2016
ISBN (Electronic)9781450335492
DOIs
Publication statusPublished - 2016 Jan 11
Externally publishedYes
Event43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016 - St. Petersburg, United States
Duration: 2016 Jan 202016 Jan 22

Other

Other43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016
CountryUnited States
CitySt. Petersburg
Period16/1/2016/1/22

Fingerprint

Acoustic waves

Keywords

  • Automata-theoretic verification
  • Automatic verification
  • Binary reachability analysis
  • CEGAR
  • Higher-order programs
  • Temporal properties

ASJC Scopus subject areas

  • Software

Cite this

Murase, A., Terauchi, T., Kobayashi, N., Sato, R., & Unno, H. (2016). Temporal verification of higher-order functional programs. In POPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Vol. 20-22-January-2016, pp. 57-68). Association for Computing Machinery. https://doi.org/10.1145/2837614.2837667

Temporal verification of higher-order functional programs. / Murase, Akihiro; Terauchi, Tachio; Kobayashi, Naoki; Sato, Ryosuke; Unno, Hiroshi.

POPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Vol. 20-22-January-2016 Association for Computing Machinery, 2016. p. 57-68.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Murase, A, Terauchi, T, Kobayashi, N, Sato, R & Unno, H 2016, Temporal verification of higher-order functional programs. in POPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. vol. 20-22-January-2016, Association for Computing Machinery, pp. 57-68, 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, United States, 16/1/20. https://doi.org/10.1145/2837614.2837667
Murase A, Terauchi T, Kobayashi N, Sato R, Unno H. Temporal verification of higher-order functional programs. In POPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Vol. 20-22-January-2016. Association for Computing Machinery. 2016. p. 57-68 https://doi.org/10.1145/2837614.2837667
Murase, Akihiro ; Terauchi, Tachio ; Kobayashi, Naoki ; Sato, Ryosuke ; Unno, Hiroshi. / Temporal verification of higher-order functional programs. POPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Vol. 20-22-January-2016 Association for Computing Machinery, 2016. pp. 57-68
@inproceedings{e540b911717a40a7bcabbdf8796e2337,
title = "Temporal verification of higher-order functional programs",
abstract = "We present an automated approach to verifying arbitrary omegaregular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the {"}calling relation{"} is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.",
keywords = "Automata-theoretic verification, Automatic verification, Binary reachability analysis, CEGAR, Higher-order programs, Temporal properties",
author = "Akihiro Murase and Tachio Terauchi and Naoki Kobayashi and Ryosuke Sato and Hiroshi Unno",
year = "2016",
month = "1",
day = "11",
doi = "10.1145/2837614.2837667",
language = "English",
volume = "20-22-January-2016",
pages = "57--68",
booktitle = "POPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",
publisher = "Association for Computing Machinery",

}

TY - GEN

T1 - Temporal verification of higher-order functional programs

AU - Murase, Akihiro

AU - Terauchi, Tachio

AU - Kobayashi, Naoki

AU - Sato, Ryosuke

AU - Unno, Hiroshi

PY - 2016/1/11

Y1 - 2016/1/11

N2 - We present an automated approach to verifying arbitrary omegaregular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the "calling relation" is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.

AB - We present an automated approach to verifying arbitrary omegaregular properties of higher-order functional programs. Previous automated methods proposed for this class of programs could only handle safety properties or termination, and our approach is the first to be able to verify arbitrary omega-regular liveness properties. Our approach is automata-theoretic, and extends our recent work on binary-reachability-based approach to automated termination verification of higher-order functional programs to fair termination published in ESOP 2014. In that work, we have shown that checking disjunctive well-foundedness of (the transitive closure of) the "calling relation" is sound and complete for termination. The extension to fair termination is tricky, however, because the straightforward extension that checks disjunctive well-foundedness of the fair calling relation turns out to be unsound, as we shall show in the paper. Roughly, our solution is to check fairness on the transition relation instead of the calling relation, and propagate the information to determine when it is necessary and sufficient to check for disjunctive well-foundedness on the calling relation. We prove that our approach is sound and complete. We have implemented a prototype of our approach, and confirmed that it is able to automatically verify liveness properties of some non-trivial higher-order programs.

KW - Automata-theoretic verification

KW - Automatic verification

KW - Binary reachability analysis

KW - CEGAR

KW - Higher-order programs

KW - Temporal properties

UR - http://www.scopus.com/inward/record.url?scp=84962532121&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84962532121&partnerID=8YFLogxK

U2 - 10.1145/2837614.2837667

DO - 10.1145/2837614.2837667

M3 - Conference contribution

AN - SCOPUS:84962532121

VL - 20-22-January-2016

SP - 57

EP - 68

BT - POPL 2016 - Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

PB - Association for Computing Machinery

ER -