More Web Proxy on the site http://driver.im/

research-article

Types and higher-order recursion schemes for verification of higher-order programs

Author:

Naoki KobayashiAuthors Info & Claims

ACM SIGPLAN Notices, Volume 44, Issue 1

Pages 416 - 428

https://doi.org/10.1145/1594834.1480933

Published: 21 January 2009 Publication History

Abstract

We propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is transformed to an HORS that generates a tree representing all the possible event sequences of the program, and then the HORS is model-checked. Unlike most of the previous methods for verification of higher-order programs, our verification method is sound and complete. Moreover, this new verification framework allows a smooth integration of abstract model checking techniques into verification of higher-order programs. We also present a type-based verification algorithm for HORS's. The algorithm can deal with only a fragment of the properties expressed by modal mu-calculus, but the algorithm and its correctness proof are (arguably) much simpler than those of Ong's game-semantics-based algorithm. Moreover, while the HORS model checking problem is n-EXPTIME in general, our algorithm is linear in the size of HORS, under the assumption that the sizes of types and specification formulas are bounded by a constant.

References

[1]

K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3), 2007.

[2]

K. Aehlig, J. G. de Miranda, and C.-H. L. Ong. The monadic second order theory of trees given by arbitrary level--tworecursion schemes is decidable. In TLCA 2005, volume 3461 of LNCS, pages 39--54.Springer-Verlag, 2005.

Digital Library

[3]

T. Ball, R. Majumdar, T. D. Millstein, and S. K. Rajamani. Automatic predicate abstraction of C programs. In PLDI 2001, pages 203--213, 2001.

Digital Library

[4]

T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL, pages 1--3, 2002.

Digital Library

[5]

D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar. The software model checker blast. International Journal on Software Tools for Technology Transfer, 9(5-6):505--525, 2007.

Digital Library

[6]

S. Chaki, S. Rajamani, and J. Rehof. Types as models: Model checking message-passing programs. In Proc. of POPL, pages 45--57, 2002.

Digital Library

[7]

B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Y. Vardi. Proving that programs eventually do something good. In Proc. of POPL, pages 265--276, 2007.

Digital Library

[8]

R. DeLine and M. Fähndrich. Adoption and focus: Practical linear types for imperative programming. In Proc. of PLDI, 2002.

Digital Library

[9]

E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS 1991, pages 368--377, 1991.

Digital Library

[10]

J. Field, D. Goyal, G.a Ramalingam, and E. Yahav. Typestate verification: Abstraction techniques and complexity Sci. Comput. Program., 58(1-2):57--82, 2005.

Digital Library

[11]

S. J. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective typestate verification in the presence of aliasing. ACM Trans. Softw. Eng. Methodol., 17(2), 2008.

Digital Library

[12]

J. S. Foster, T. Terauchi, and A. Aiken. ACM Trans. Softw. Eng. Methodol., 17(2), 2008. In Proc. of PLDI, pages 1--12, 2002.

Digital Library

[13]

C. Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. Science of Computer Programming, 50(1-3):189--224, 2004.

Digital Library

[14]

M. Hague and C.-H. L. Ong. Symbolic backwards-reachability analysis for higher-order pushdown In FoSSaCS 2007, volume 4423 of LNCS, pages 213--227. Springer-Verlag, 2007.

Digital Library

[15]

N. Heintze and D. A. McAllester. Linear-time subtransitive control flow analysis. In Proc. of PLDI, pages 261--272, 1997.

Digital Library

[16]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Proc. of POPL, pages 58--70, 2002.

Digital Library

[17]

H. Hosoya, J. Vouillon, and B. C. Pierce. Regular expression types for xml. ACM Trans. Program. Lang. Syst., 27(1):46--90, 2005.

Digital Library

[18]

A. Igarashi and N. Kobayashi. A generic type system for the pi-calculus. Theor. Comput. Sci., 311(1-3):121--163, 2004.

Digital Library

[19]

A. Igarashi and N. Kobayashi. Resource usage analysis. ACM Trans. Prog. Lang. Syst., 27(2):264--313, 2005. Preliminary summary appeared in Proceedings of POPL 2002.

Digital Library

[20]

F. Iwama, A. Igarashi, and N. Kobayashi. Resource usage analysis for a functional language with exceptions. In Proceedings of ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation (PEPM 2006), pages 38--47. ACM Press, 2006.

Digital Library

[21]

D. Kikuchi and N. Kobayashi. Type-based verification of correspondence assertions for communication protocols. In Proceedings of APLAS 2007, volume 4807 of LNCS, pages 191--205. Springer-Verlag, 2007.

Digital Library

[22]

T. Knapik, D. Niwinski, and P. Urzyczyn. Deciding monadic theories of hyperalgebraic trees. Deciding monadic theories of hyperalgebraic trees. Springer-Verlag, 2001.

[23]

T. Knapik, D. Niwinski, and P. Urzyczyn. Higher-order pushdown trees are easy. In FoSSaCS 2002, volume 2303 of LNCS, pages 205--222. Springer-Verlag, 2002.

Digital Library

[24]

T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe grammars and panic automata. Unsafe grammars and panic automata. Springer-Verlag, 2005.

[25]

N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. An extended version, available from http://www.kb.ecei.tohoku.ac.jp/ koba/papers/hors.pdf, 2008.

[26]

P. Lam, V. Kuncak, and M. C. Rinard. Generalized typestate checking for data structure consistency. In VMCAI 2005, volume 3385 of LNCS, pages 430--447.Springer-Verlag, 2005.

Digital Library

[27]

M. Naik. A type system equivalent to a model checker. Master Thesis, Purdue University.

[28]

M. Naik and J. Palsberg. A type system equivalent to a model checker. In ESOP 2005, volume 3444 of LNCS, pages 374--388. Springer-Verlag, 2005.

Digital Library

[29]

C.-H. L. Ong. On model-checking trees generated by higher-order recursion schemes. In LICS 2006, pages 81--90. IEEE Computer Society Press, 2006.

Digital Library

[30]

J. Rehof and T. Mogensen. Tractable constraints in finite semilattices. Science of Computer Programming, 35(2):191--221, 1999.

Digital Library

[31]

P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI 2008, pages 159--169, 2008.

Digital Library

[32]

R. E. Strom and S. Yemini. Typestate: A programming language concept for enhancing software reliability. Transactions on Software Engineering, 12(1):157--171, 1986.

Digital Library

[33]

W. Thomas. Languages, automata, and logic. In Handbook of formal languages, vol. 3, pages 389--455, 1997.

[34]

H. Unno and N. Kobayashi. On-demand refinement of dependent types. In Proceedings of FLOPS 2008, volume 4989 of LNCS, pages 81--96. Springer-Verlag, 2008.

Digital Library

Cited By

Jochems JJones ERamsay S(2023)Higher-Order MSL Horn ConstraintsProceedings of the ACM on Programming Languages10.1145/35712627:POPL(2017-2047)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571262
Li GMurawski AOng L(2022)Probabilistic Verification Beyond Context-FreenessProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533351(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533351
Morard DAguiar AChiba SBoix E(2020)A formalism to model higher-order functionCompanion Proceedings of the 4th International Conference on Art, Science, and Engineering of Programming10.1145/3397537.3398479(219-220)Online publication date: 23-Mar-2020
https://dl.acm.org/doi/10.1145/3397537.3398479
Show More Cited By

Index Terms

Types and higher-order recursion schemes for verification of higher-order programs

Recommendations

Types and higher-order recursion schemes for verification of higher-order programs
POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is ...
On the relationship between higher-order recursion schemes and higher-order fixpoint logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

We study the relationship between two kinds of higher-order extensions

of model checking: HORS model checking, where models are extended to

higher-order recursion schemes, and HFL model checking, where the

logic is extedned to higher-order modal ...
On the relationship between higher-order recursion schemes and higher-order fixpoint logic
POPL '17

We study the relationship between two kinds of higher-order extensions

of model checking: HORS model checking, where models are extended to

higher-order recursion schemes, and HFL model checking, where the

logic is extedned to higher-order modal ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 44, Issue 1

POPL '09

January 2009

453 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1594834

Issue’s Table of Contents

POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
January 2009
464 pages
ISBN:9781605583792
DOI:10.1145/1480881
General Chair:
Zhong Shao
Yale University, USA
,
Program Chair:
Benjamin C. Pierce
University of Pennsylvania, USA

Copyright © 2009 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: 21 January 2009

Published in SIGPLAN Volume 44, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

160
Total Citations
View Citations
777
Total Downloads

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

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Jochems JJones ERamsay S(2023)Higher-Order MSL Horn ConstraintsProceedings of the ACM on Programming Languages10.1145/35712627:POPL(2017-2047)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571262
Li GMurawski AOng L(2022)Probabilistic Verification Beyond Context-FreenessProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533351(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533351
Morard DAguiar AChiba SBoix E(2020)A formalism to model higher-order functionCompanion Proceedings of the 4th International Conference on Art, Science, and Engineering of Programming10.1145/3397537.3398479(219-220)Online publication date: 23-Mar-2020
https://dl.acm.org/doi/10.1145/3397537.3398479
Afshari BHetzl SLeigh G(2020)Herbrand's theorem as higher order recursionAnnals of Pure and Applied Logic10.1016/j.apal.2020.102792171:6(102792)Online publication date: Jun-2020
https://doi.org/10.1016/j.apal.2020.102792
Kobayashi NLago UGrellois CBouyer P(2019)On the termination problem for probabilistic higher-order recursive programsProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470177(1-14)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470177
Kobayashi NKomendantskaya E(2019)10 Years of the Higher-Order Model Checking Project (Extended Abstract)Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming10.1145/3354166.3354167(1-2)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1145/3354166.3354167
Watanabe KTsukada TOshikawa HKobayashi NHermenegildo MIgarashi A(2019)Reduction from branching-time property verification of higher-order programs to HFL validity checkingProceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation10.1145/3294032.3294077(22-34)Online publication date: 14-Jan-2019
https://dl.acm.org/doi/10.1145/3294032.3294077
Kobayashi NDal Lago UGrellois C(2019)On the Termination Problem for Probabilistic Higher-Order Recursive Programs2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS.2019.8785679(1-14)Online publication date: Jun-2019
https://doi.org/10.1109/LICS.2019.8785679
Okuyama YTsukada TKobayashi N(2019)A Temporal Logic for Higher-Order Functional ProgramsStatic Analysis10.1007/978-3-030-32304-2_21(437-458)Online publication date: 2-Oct-2019
https://doi.org/10.1007/978-3-030-32304-2_21
Nanjo YUnno HKoskinen ETerauchi T(2018)A Fixpoint Logic and Dependent Effects for Temporal Property VerificationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3209108.3209204(759-768)Online publication date: 9-Jul-2018
https://dl.acm.org/doi/10.1145/3209108.3209204
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