research-article

Predicate abstraction and CEGAR for higher-order model checking

Authors:

Naoki Kobayashi,

Hiroshi UnnoAuthors Info & Claims

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 222 - 233

https://doi.org/10.1145/1993498.1993525

Published: 04 June 2011 Publication History

Abstract

Higher-order model checking (more precisely, the model checking of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties of programs written in the simply-typed λ-calculus with recursion and finite data domains. This paper formalizes predicate abstraction and counterexample-guided abstraction refinement (CEGAR) for higher-order model checking, enabling automatic verification of programs that use infinite data domains such as integers. A prototype verifier for higher-order functional programs based on the formalization has been implemented and tested for several programs.

References

[1]

A. Bakewell and D. R. Ghica. Compositional predicate abstraction from game semantics. In TACAS '09, pages 62--76. Springer, 2009.

Digital Library

[2]

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

Digital Library

[3]

T. Ball, T. Millstein, and S. K. Rajamani. Polymorphic predicate abstraction. ACM Transactions on Programming Languages and Systems, 27(2):314--343, 2005.

Digital Library

[4]

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

Digital Library

[5]

C. Barrett and C. Tinelli. CVC3. In CAV '07, volume 4590 of LNCS, pages 298--302. Springer, July 2007.

Digital Library

[6]

D. Beyer, D. Zufferey, and R. Majumdar. CSIsat: Interpolation for LA EUF (tool paper). In CAV '08, volume 5123 of LNCS, pages 304--308, July 2008.

Digital Library

[7]

W.-N. Chin and S.-C. Khoo. Calculating sized types. Higher-Order and Symbolic Computation, 14(2-3):261--300, September 2001.

Digital Library

[8]

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM, 50(5):752--794, 2003.

Digital Library

[9]

P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL '78, pages 84--96. ACM, 1978.

Digital Library

[10]

W. Damm. The IO- and OI-hierarchies. Theoretical Computer Science, 20(2):95--207, 1982.

[11]

C. Flanagan. Hybrid type checking. In POPL '06, pages 245--256. ACM, 2006.

Digital Library

[12]

S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In CAV '97, volume 1254 of LNCS, pages 72--83. Springer, June 1997.

Digital Library

[13]

M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In POPL '10, pages 471--482. ACM, 2010.

Digital Library

[14]

T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL '04, pages 232--244. ACM, 2004.

Digital Library

[15]

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

Digital Library

[16]

R. Jhala and R. Majumdar. Counterexample refinement for functional programs. Manuscript, available from http://www.cs.ucla.edu/ rupak/Papers/CEGARFunctional.ps, 2009.

[17]

R. Jhala, R. Majumdar, and A. Rybalchenko. Refinement type inference via abstract interpretation. arXiv:1004.2884v1, 2010.

[18]

R. Jhala and K. L. McMillan. A practical and complete approach to predicate refinement. In TACAS '06, volume 3920 of LNCS, pages 459--473. Springer, 2006.

Digital Library

[19]

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

Digital Library

[20]

N. Kobayashi. Model-checking higher-order functions. In PPDP '09, pages 25--36. ACM, 2009.

Digital Library

[21]

N. Kobayashi. TRecS. http://www.kb.ecei.tohoku.ac.jp/koba/trecs/, 2009.

[22]

N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL '09, pages 416--428. ACM, 2009.

Digital Library

[23]

N. Kobayashi. A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes. In FoSSaCS '11. Springer, 2011.

Digital Library

[24]

N. Kobayashi and C.-H. L. Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In LICS '09, pages 179--188. IEEE, 2009.

Digital Library

[25]

N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for higher-order model checking. An extended version, available from http://www.kb.ecei.tohoku.ac.jp/ uhiro/, 2011.

[26]

N. Kobayashi, N. Tabuchi, and H. Unno. Higher-order multi-parameter tree transducers and recursion schemes for program verification. In POPL '10, pages 495--508. ACM, 2010.

Digital Library

[27]

K. L. McMillan. An interpolating theorem prover. Theoretical Computer Science, 345(1):101--121, 2005.

Digital Library

[28]

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

Digital Library

[29]

C.-H. L. Ong and S. J. Ramsay. Verifying higher-order functional programs with pattern-matching algebraic data types. In POPL '11, pages 587--598. ACM, 2011.

Digital Library

[30]

J. C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of the ACM annual conference - Volume 2, pages 717--740. ACM, 1972.

Digital Library

[31]

P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI '08. ACM, 2008.

Digital Library

[32]

T. Terauchi. Dependent types from counterexamples. In POPL '10, pages 119--130. ACM, 2010.

Digital Library

[33]

H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP '09, pages 277--288. ACM, 2009.

Digital Library

[34]

H. Unno, N. Tabuchi, and N. Kobayashi. Verification of tree-processing programs via higher-order model checking. In APLAS '10, volume 6461 of LNCS, pages 312--327. Springer, October/December 2010.

Digital Library

[35]

H. Xi and F. Pfenning. Dependent types in practical programming. In POPL '99, pages 214--227. ACM, 1999.

Digital Library

Cited By

Sekiyama TUnno H(2024)Higher-Order Model Checking of Effect-Handling Programs with Answer-Type ModificationProceedings of the ACM on Programming Languages10.1145/36898058:OOPSLA2(2662-2691)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689805
Tanaka ISakayori KKobayashi NKeller GWang M(2024)Ownership Types for Verification of Programs with Pointer ArithmeticProceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation10.1145/3635800.3636965(94-106)Online publication date: 11-Jan-2024
https://dl.acm.org/doi/10.1145/3635800.3636965
Faella MGarbi GLa Torre SParlato G(2024)CHC-Based Verification of Programs Through Graph DecompositionsSN Computer Science10.1007/s42979-024-03371-65:8Online publication date: 18-Nov-2024
https://doi.org/10.1007/s42979-024-03371-6
Show More Cited By

Index Terms

Predicate abstraction and CEGAR for higher-order model checking

Recommendations

Predicate abstraction and CEGAR for higher-order model checking
PLDI '11

Higher-order model checking (more precisely, the model checking of higher-order recursion schemes) has been extensively studied recently, which can automatically decide properties of programs written in the simply-typed λ-calculus with recursion and ...
Combining Theorem Proving with Model Checking through Predicate Abstraction

This article presents a procedure for proving invariants of infinite-state reactive systems using a combination of two formal verification techniques: theorem proving and model checking. This method uses term rewriting on the definition of the target ...
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2011

668 pages

ISBN:9781450306638

DOI:10.1145/1993498

General Chair:
Mary Hall
University of Utah
,
Program Chair:
David Padua
University of Illinois at Urbana-Champaign

ACM SIGPLAN Notices Volume 46, Issue 6
PLDI '11
June 2011
652 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1993316
Issue’s Table of Contents

Copyright © 2011 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]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 June 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '11

Sponsor:

SIGPLAN

PLDI '11: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 4 - 8, 2011

California, San Jose, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

140
Total Citations
View Citations
607
Total Downloads

Downloads (Last 12 months)46
Downloads (Last 6 weeks)5

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Sekiyama TUnno H(2024)Higher-Order Model Checking of Effect-Handling Programs with Answer-Type ModificationProceedings of the ACM on Programming Languages10.1145/36898058:OOPSLA2(2662-2691)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689805
Tanaka ISakayori KKobayashi NKeller GWang M(2024)Ownership Types for Verification of Programs with Pointer ArithmeticProceedings of the 2024 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation10.1145/3635800.3636965(94-106)Online publication date: 11-Jan-2024
https://dl.acm.org/doi/10.1145/3635800.3636965
Faella MGarbi GLa Torre SParlato G(2024)CHC-Based Verification of Programs Through Graph DecompositionsSN Computer Science10.1007/s42979-024-03371-65:8Online publication date: 18-Nov-2024
https://doi.org/10.1007/s42979-024-03371-6
Katsura HKobayashi NSakayori KSato R(2024)Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability ProblemProgramming Languages and Systems10.1007/978-981-97-8943-6_16(325-345)Online publication date: 23-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8943-6_16
Bajczi LMolnár V(2024)Solving Constrained Horn Clauses as C Programs with CHC2CModel Checking Software10.1007/978-3-031-66149-5_8(146-163)Online publication date: 10-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-66149-5_8
Sato R(2023)Refinement Types for Call-by-name ProgramsJournal of Information Processing10.2197/ipsjjip.31.70831(708-721)Online publication date: 2023
https://doi.org/10.2197/ipsjjip.31.708
Katsura HKobayashi NSato R(2023)Higher-Order Property-Directed ReachabilityProceedings of the ACM on Programming Languages10.1145/36078317:ICFP(48-77)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607831
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
Farzan ANicolet V(2023)Partial bounding for recursive function synthesisFormal Methods in System Design10.1007/s10703-023-00417-y63:1-3(172-205)Online publication date: 16-May-2023
https://doi.org/10.1007/s10703-023-00417-y
Pasquier MTeodorov CJouault FBrun MRoux LLagadec LSyriani ESahraoui H(2022)Practical multiverse debugging through user-defined reductionsProceedings of the 25th International Conference on Model Driven Engineering Languages and Systems10.1145/3550355.3552447(87-97)Online publication date: 23-Oct-2022
https://dl.acm.org/doi/10.1145/3550355.3552447
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 Table of Contents