article

Temporal verification of higher-order functional programs

Authors:

Akihiro Murase,

Tachio Terauchi,

Naoki Kobayashi,

Hiroshi UnnoAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 1

Pages 57 - 68

https://doi.org/10.1145/2914770.2837667

Published: 11 January 2016 Publication History

Abstract

We present an automated approach to verifying arbitrary omega-regular 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.

References

[1]

A. M. Ben-Amram. General size-change termination and lexicographic descent. In T. Æ. Mogensen, D. A. Schmidt, and I. H. Sudborough, editors, The Essence of Computation, Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones {on occasion of his 60th birthday}, volume 2566 of Lecture Notes in Computer Science, pages 3–17. Springer, 2002.

Digital Library

[2]

B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Y. Vardi. Proving that programs eventually do something good. In M. Hofmann and M. Felleisen, editors, Proceedings of the 34th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 265–276. ACM, 2007.

Digital Library

[3]

B. Cook and E. Koskinen. Making prophecies with decision predicates. In T. Ball and M. Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 399–410. ACM, 2011.

Digital Library

[4]

B. Cook and E. Koskinen. Reasoning about nondeterminism in programs. In H. Boehm and C. Flanagan, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, pages 219–230. ACM, 2013.

Digital Library

[5]

B. Cook, E. Koskinen, and M. Y. Vardi. Temporal property verification as a program analysis task. In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 333–348. Springer, 2011.

Digital Library

[6]

B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In M. I. Schwartzbach and T. Ball, editors, Proceedings of the ACM SIGPLAN 2006 Conference on Programming Language Design and Implementation, Ottawa, Ontario, Canada, June 11-14, 2006, pages 415–426. ACM, 2006.

Digital Library

[7]

B. Cook, A. See, and F. Zuleger. Ramsey vs. lexicographic termination proving. In TACAS, volume 7795 of Lecture Notes in Computer Science, pages 47–61. Springer, 2013.

Digital Library

[8]

L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, volume 4963 of Lecture Notes in Computer Science, pages 337–340. Springer, 2008.

Digital Library

[9]

K. Fujima, S. Ito, and N. Kobayashi. Practical alternating parity tree automata model checking of higher-order recursion schemes. In C. Shan, editor, Programming Languages and Systems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9- 11, 2013. Proceedings, volume 8301 of Lecture Notes in Computer Science, pages 17–32. Springer, 2013.

Digital Library

[10]

J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann. Automated termination proofs for Haskell by term rewriting. ACM Trans. Prog. Lang. Syst., 33(2):7:1–7:39, Feb. 2011.

Digital Library

[11]

M. Hofmann and W. Chen. Abstract interpretation from Büchi automata. In T. A. Henzinger and D. Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014, pages 51:1–51:10. ACM, 2014.

Digital Library

[12]

M. Hofmann and W. Chen. Büchi types for infinite traces and liveness. CoRR, abs/1401.5107, 2014.

[13]

R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: verifying functional programs using abstract interpreters. In G. Gopalakrishnan and S. Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 470–485. Springer, 2011.

Digital Library

[14]

T. Johnsson. Lambda lifting: Treansforming programs to recursive equations. In FPCA, pages 190–203, 1985.

Digital Library

[15]

N. D. Jones and N. Bohr. Call-by-value termination in the untyped lambda-calculus. Logical Methods in Computer Science, 4(1), 2008.

[16]

N. Kobayashi and C. L. Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 179–188. IEEE Computer Society, 2009.

Digital Library

[17]

N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for higher-order model checking. In M. W. Hall and D. A. Padua, editors, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pages 222–233. ACM, 2011.

Digital Library

[18]

E. Koskinen and T. Terauchi. Local temporal reasoning. In T. A. Henzinger and D. Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014, pages 59:1–59:10. ACM, 2014.

Digital Library

[19]

T. Kuwahara, R. Sato, H. Unno, and N. Kobayashi. Predicate abstraction and CEGAR for disproving termination of higher-order functional programs. In D. Kroening and C. S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II, volume 9207 of Lecture Notes in Computer Science, pages 287–303. Springer, 2015.

[20]

T. Kuwahara, T. Terauchi, H. Unno, and N. Kobayashi. Automatic termination verification for higher-order functional programs. In Z. Shao, editor, Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8410 of Lecture Notes in Computer Science, pages 392–411. Springer, 2014.

[21]

M. M. Lester, R. P. Neatherway, C.-H. L. Ong, and S. J. Ramsay. Model checking liveness properties of higher-order functional programs. URL https://mjolnir.comlab.ox.ac.uk/papers/ thors.pdf, 2011.

[22]

R. P. Neatherway and C. L. Ong. TravMC2: higher-order model checking for alternating parity tree automata. In N. Rungta and O. Tkachuk, editors, 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, July 21-23, 2014, pages 129–132. ACM, 2014.

Digital Library

[23]

C. L. Ong. On model-checking trees generated by higher-order recursion schemes. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81–90. IEEE Computer Society, 2006.

Digital Library

[24]

A. Pnueli, A. Podelski, and A. Rybalchenko. Separating fairness and well-foundedness for the analysis of fair discrete systems. In N. Halbwachs and L. D. Zuck, editors, Tools and Algorithms for the Construction and Analysis of Systems, 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, volume 3440 of Lecture Notes in Computer Science, pages 124–139. Springer, 2005.

Digital Library

[25]

A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI, volume 2937 of Lecture Notes in Computer Science, pages 239–251. Springer, 2004.

[26]

A. Podelski and A. Rybalchenko. Transition invariants. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 32–41. IEEE Computer Society, 2004.

Digital Library

[27]

P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In R. Gupta and S. P. Amarasinghe, editors, Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pages 159–169. ACM, 2008.

Digital Library

[28]

R. Sato, H. Unno, and N. Kobayashi. Towards a scalable software model checker for higher-order programs. In E. Albert and S. Mu, editors, Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013, Rome, Italy, January 21-22, 2013, pages 53–62. ACM, 2013.

Digital Library

[29]

D. Sereni. Termination analysis of higher-order functional programs. PhD thesis, Magdalen College, 2006.

[30]

C. Skalka and S. F. Smith. History effects and verification. In W. Chin, editor, Programming Languages and Systems: Second Asian Symposium, APLAS 2004, Taipei, Taiwan, November 4-6, 2004. Proceedings, volume 3302 of Lecture Notes in Computer Science, pages 107–128. Springer, 2004.

[31]

C. Skalka, S. F. Smith, and D. V. Horn. Types and trace effects of higher order programs. J. Funct. Program., 18(2):179–249, 2008.

Digital Library

[32]

T. Terauchi. Dependent types from counterexamples. In M. V. Hermenegildo and J. Palsberg, editors, Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pages 119– 130. ACM, 2010.

Digital Library

[33]

H. Unno and N. Kobayashi. Dependent type inference with interpolants. In A. Porto and F. J. L ´opez-Fraguas, editors, Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, pages 277–288. ACM, 2009.

Digital Library

[34]

H. Unno, T. Terauchi, and N. Kobayashi. Automating relatively complete verification of higher-order functional programs. In R. Giacobazzi and R. Cousot, editors, The 40th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25, 2013, pages 75–86. ACM, 2013.

Digital Library

[35]

M. Y. Vardi. Verification of concurrent programs: The automatatheoretic framework. Ann. Pure Appl. Logic, 51(1-2):79–98, 1991.

[36]

N. Vazou, E. L. Seidel, and R. Jhala. LiquidHaskell: experience with refinement types in the real world. In W. Swierstra, editor, Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, Gothenburg, Sweden, September 4-5, 2014, pages 39–51. ACM, 2014.

Digital Library

[37]

N. Vazou, E. L. Seidel, R. Jhala, D. Vytiniotis, and S. L. P. Jones. Refinement types for Haskell. In J. Jeuring and M. M. T. Chakravarty, editors, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, pages 269–282. ACM, 2014.

Digital Library

[38]

K. Yokoyama. Ramsey’s theorem and termination analysis. In JAIST RCSV-Logic Workshop, 2014. http://www.jaist.ac.jp/rcsv/ event/20141030-eventws/yokoyama.pdf.

Cited By

Song YChin W(2020)Automated Temporal Verification of Integrated Dependent EffectsFormal Methods and Software Engineering10.1007/978-3-030-63406-3_5(73-90)Online publication date: 19-Dec-2020
https://doi.org/10.1007/978-3-030-63406-3_5
Walukiewicz IBouyer P(2019)LambdaY-calculus with prioritiesProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470172(1-13)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470172
Kobayashi NTsukada TWatanabe K(2018)Higher-Order Program Verification via HFL Model CheckingProgramming Languages and Systems10.1007/978-3-319-89884-1_25(711-738)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89884-1_25
Show More Cited By

Recommendations

Temporal verification of higher-order functional programs
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

We present an automated approach to verifying arbitrary omega-regular 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 ...
Automatically disproving fair termination of higher-order functional programs
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

We propose an automated method for disproving fair termination of higher-order functional programs, which is complementary to Murase et al.’s recent method for proving fair termination. A program is said to be fair terminating if it has no infinite ...
Automatically disproving fair termination of higher-order functional programs
ICFP '16

We propose an automated method for disproving fair termination of higher-order functional programs, which is complementary to Murase et al.’s recent method for proving fair termination. A program is said to be fair terminating if it has no infinite ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 51, Issue 1

POPL '16

January 2016

815 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2914770

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2016
815 pages
ISBN:9781450335492
DOI:10.1145/2837614
General Chair:
Rastislav Bodik
UC Berkeley, USA
,
Program Chair:
Rupak Majumdar
MPI-SWS, Germany

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2016

Published in SIGPLAN Volume 51, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

31
Total Citations
View Citations
310
Total Downloads

Downloads (Last 12 months)27
Downloads (Last 6 weeks)1

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Song YChin W(2020)Automated Temporal Verification of Integrated Dependent EffectsFormal Methods and Software Engineering10.1007/978-3-030-63406-3_5(73-90)Online publication date: 19-Dec-2020
https://doi.org/10.1007/978-3-030-63406-3_5
Walukiewicz IBouyer P(2019)LambdaY-calculus with prioritiesProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470172(1-13)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470172
Kobayashi NTsukada TWatanabe K(2018)Higher-Order Program Verification via HFL Model CheckingProgramming Languages and Systems10.1007/978-3-319-89884-1_25(711-738)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89884-1_25
Unno HSatake YTerauchi T(2017)Relatively complete refinement type system for verification of higher-order non-deterministic programsProceedings of the ACM on Programming Languages10.1145/31581002:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158100
Nakamura HKojima KSuenaga KIgarashi A(2017)A Nonstandard Functional Programming LanguageProgramming Languages and Systems10.1007/978-3-319-71237-6_25(514-533)Online publication date: 19-Nov-2017
https://doi.org/10.1007/978-3-319-71237-6_25
Walukiewicz I(2016)Automata theory and higher-order model-checkingACM SIGLOG News10.1145/3026744.30267453:4(13-31)Online publication date: 15-Dec-2016
https://dl.acm.org/doi/10.1145/3026744.3026745
Sekiyama TUnno H(2023)Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited ContinuationsProceedings of the ACM on Programming Languages10.1145/35712647:POPL(2079-2110)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571264
Kobayashi NTanahashi KSato RTsukada T(2023)HFL(Z) Validity Checking for Automated Program VerificationProceedings of the ACM on Programming Languages10.1145/35711997:POPL(154-184)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571199
Kobayashi N(2021)An Overview of the HFL Model Checking ProjectElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.344.1344(1-12)Online publication date: 13-Sep-2021
https://doi.org/10.4204/EPTCS.344.1
Jaber GRiba C(2021)Temporal Refinements for Guarded Recursive TypesProgramming Languages and Systems10.1007/978-3-030-72019-3_20(548-578)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_20
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents