research-article

Learning refinement types

Authors:

Aditya V. Nori,

Suresh JagannathanAuthors Info & Claims

ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming

Pages 400 - 411

https://doi.org/10.1145/2784731.2784766

Published: 29 August 2015 Publication History

Abstract

We propose the integration of a random test generation system (capable of discovering program bugs) and a refinement type system (capable of expressing and verifying program invariants), for higher-order functional programs, using a novel lightweight learning algorithm as an effective intermediary between the two. Our approach is based on the well-understood intuition that useful, but difficult to infer, program properties can often be observed from concrete program states generated by tests; these properties act as likely invariants, which if used to refine simple types, can have their validity checked by a refinement type checker. We describe an implementation of our technique for a variety of benchmarks written in ML, and demonstrate its effectiveness in inferring and proving useful invariants for programs that express complex higher-order control and dataflow.

References

[1]

A. Albarghouthi and K. L. McMillan. Beautiful interpolants. In CAV, 2013.

Digital Library

[2]

D. Beyer and M. E. Keremoglu. Cpachecker: A tool for configurable software verification. In CAV, 2011.

Digital Library

[3]

C. Boyapati, S. Khurshid, and D. Marinov. Korat: Automated testing based on java predicates. In ISSTA, 2002.

Digital Library

[4]

H. R. Chamarthi, P. C. Dillinger, M. Kaufmann, and P. Manolios. Integrating testing and interactive theorem proving. In ACL2, 2011.

[5]

R. Chugh, P. M. Rondon, and R. Jhala. Nested refinements: A logic for duck typing. In POPL, 2012.

Digital Library

[6]

K. Claessen and J. Hughes. Quickcheck: A lightweight tool for random testing of haskell programs. In ICFP, 2000.

Digital Library

[7]

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexampleguided abstraction refinement for symbolic model checking. J. ACM, 50(5):752–794, 2003.

Digital Library

[8]

M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program., 69(1-3):35–45, 2007.

Digital Library

[9]

C. Flanagan and K. R. M. Leino. Houdini, an annotation assistant for esc/java. In FME, 2001.

Digital Library

[10]

P. Garg, C. Löding, P. Madhusudan, and D. Neider. Ice: A robust learning framework for learning invariants. In CAV, 2014.

Digital Library

[11]

S. Graf and H. Sa¨ıdi. Construction of abstract state graphs with pvs. In CAV, 1997.

Digital Library

[12]

B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori, and S. K. Rajamani. Synergy: A new algorithm for property checking. In FSE, 2006.

Digital Library

[13]

T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL, 2004.

Digital Library

[14]

R. Jhala, R. Majumdar, and A. Rybalchenko. Hmc: Verifying functional programs using abstract interpreters. In CAV, 2011.

Digital Library

[15]

M. Kawaguchi, P. Rondon, and R. Jhala. Type-based data structure verification. In PLDI, 2009.

Digital Library

[16]

N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL, 2009.

Digital Library

[17]

N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and cegar for higher-order model checking. In PLDI, 2011.

Digital Library

[18]

S. Lindley and C. McBride. Hasochism: The pleasure and pain of dependently typed haskell programming. In Haskell, 2013.

Digital Library

[19]

C. McBride. Faking it simulating dependent types in haskell. J. Funct. Program., 12(5):375–392, 2002.

Digital Library

[20]

E. J. McCluskey. Minimization of boolean functions. Bell system technical Journal, 35(6):1417–1444, 1956.

[21]

K. L. McMillan. An interpolating theorem prover. Theor. Comput. Sci., 345(1):101–121, 2005.

Digital Library

[22]

A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau, and L. Birkedal. Ynot: Dependent types for imperative programs. In ICFP, 2008.

Digital Library

[23]

C. G. Nelson. Techniques for program verification. Technical report, XEROX Research Center, 1981.

[24]

P. C. Nguyen and D. V. Horn. Relatively complete counterexamples for higher-order programs. In PLDI, 2015.

Digital Library

[25]

T. Nguyen, D. Kapur, W. Weimer, and S. Forrest. Using dynamic analysis to discover polynomial and array invariants. In ICSE, 2012.

Digital Library

[26]

OCAML Library. http://caml.inria.fr/pub/docs/.

[27]

S. J. Ramsay, R. P. Neatherway, and C.-H. L. Ong. A type-directed abstraction refinement approach to higher-order model checking. In POPL, 2014.

Digital Library

[28]

P. M. Rondon, M. Kawaguci, and R. Jhala. Liquid types. In PLDI, 2008.

Digital Library

[29]

E. L. Seidel, N. Vazou, and R. Jhala. Type targeted testing. In ESOP, 2015.

Digital Library

[30]

R. Sharma and A. Aiken. From invariant checking to invariant inference using randomized search. In CAV, 2014.

Digital Library

[31]

R. Sharma, M. Gligoric, A. Arcuri, G. Fraser, and D. Marinov. Testing container classes: Random or systematic? In FASE, 2011.

Digital Library

[32]

R. Sharma, A. V. Nori, and A. Aiken. Interpolants as classifiers. In CAV, 2012.

Digital Library

[33]

R. Sharma, S. Gupta, B. Hariharan, A. Aiken, P. Liang, and A. V. Nori. A data driven approach for algebraic loop invariants. In ESOP, 2013.

Digital Library

[34]

R. Sharma, S. Gupta, B. Hariharan, A. Aiken, and A. V. Nori. Verification as learning geometric concepts. In SAS, 2013.

[35]

SML Library. http://www.smlnj.org/doc/smlnj-lib/.

[36]

N. Swamy, J. Weinberger, C. Schlesinger, J. Chen, and B. Livshits. Verifying higher-order programs with the dijkstra monad. In PLDI, 2013.

Digital Library

[37]

T. Terauchi. Dependent types from counterexamples. In POPL, 2010.

Digital Library

[38]

H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP, 2009.

Digital Library

[39]

H. Unno, T. Terauchi, and N. Kobayashi. Automating relatively complete verification of higher-order functional programs. In POPL, 2013.

Digital Library

[40]

N. Vazou, P. M. Rondon, and R. Jhala. Abstract refinement types. In ESOP, 2013.

Digital Library

[41]

H. Xi and F. Pfenning. Dependent types in practical programming. In POPL, 1999.

Digital Library

[42]

Yices SMT solver. http://yices.csl.sri.com/.

[43]

H. Zhu and S. Jagannathan. Compositional and lightweight dependent type inference for ml. In VMCAI, 2013.

Digital Library

[44]

H. Zhu, A. V. Nori, and S. Jagannathan. Learning refinement types. Technical report, Purdue Univsersity, 2015.

[45]

https://www.cs. purdue.edu/homes/zhu103/msolve/tech.pdf.

Cited By

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
Yu SWang TWang JJust RFraser G(2023)Loop Invariant Inference through SMT Solving Enhanced Reinforcement LearningProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598047(175-187)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598047
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
Show More Cited By

Index Terms

Learning refinement types

Recommendations

Learning refinement types
ICFP '15

We propose the integration of a random test generation system (capable of discovering program bugs) and a refinement type system (capable of expressing and verifying program invariants), for higher-order functional programs, using a novel lightweight ...
Mechanizing Refinement Types

Practical checkers based on refinement types use the combination of implicit semantic subtyping and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal ...
Refinement types for Haskell
PLPV '14: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages meets Program Verification

We present LiquidHaskell (http://goto.ucsd.edu/liquid), an automatic verifier for Haskell. LiquidHaskell uses Refinement types, a restricted form of dependent types where relationships between values are encoded by decorating types with logical ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming

August 2015

436 pages

ISBN:9781450336697

DOI:10.1145/2784731

General Chair:
Kathleen Fisher
Tufts University, USA
,
Program Chair:
John Reppy
University of Chicago, USA

ACM SIGPLAN Notices Volume 50, Issue 9
ICFP '15
September 2015
436 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2858949
Editor:
Andy Gill
University of Kansas, Lawrence, KS
Issue’s Table of Contents

Copyright © 2015 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: 29 August 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Conference

ICFP'15

Sponsor:

SIGPLAN

ICFP'15: 20th ACM SIGPLAN International Conference on Functional Programming

August 31 - September 2, 2015

BC, Vancouver, Canada

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
323
Total Downloads

Downloads (Last 12 months)30
Downloads (Last 6 weeks)6

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
Yu SWang TWang JJust RFraser G(2023)Loop Invariant Inference through SMT Solving Enhanced Reinforcement LearningProceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3597926.3598047(175-187)Online publication date: 12-Jul-2023
https://dl.acm.org/doi/10.1145/3597926.3598047
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
Mukai RKobayashi NSato R(2022)Parameterized Recursive Refinement Types for Automated Program VerificationStatic Analysis10.1007/978-3-031-22308-2_18(397-421)Online publication date: 2-Dec-2022
https://doi.org/10.1007/978-3-031-22308-2_18
Pavlinovic ZSu YWies T(2021)Data flow refinement type inferenceProceedings of the ACM on Programming Languages10.1145/34343005:POPL(1-31)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434300
Unno HTerauchi TKoskinen E(2021)Constraint-Based Relational VerificationComputer Aided Verification10.1007/978-3-030-81685-8_35(742-766)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81685-8_35
Iwayama NKobayashi NSuzuki RTsukada T(2021)Predicate Abstraction and CEGAR for $$\nu \mathrm {HFL}_\mathbb {Z}$$ Validity CheckingStatic Analysis10.1007/978-3-030-65474-0_7(134-155)Online publication date: 13-Jan-2021
https://doi.org/10.1007/978-3-030-65474-0_7
Ezudheen PNeider DD'Souza DGarg PMadhusudan P(2018)Horn-ICE learning for synthesizing invariants and contractsProceedings of the ACM on Programming Languages10.1145/32765012:OOPSLA(1-25)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276501
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
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
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