skip to main content
research-article

Automating relatively complete verification of higher-order functional programs

Published: 23 January 2013 Publication History

Abstract

We present an automated approach to relatively completely verifying safety (i.e., reachability) property of higher-order functional programs. Our contribution is two-fold. First, we extend the refinement type system framework employed in the recent work on (incomplete) automated higher-order verification by drawing on the classical work on relatively complete "Hoare logic like" program logic for higher-order procedural languages. Then, by adopting the recently proposed techniques for solving constraints over quantified first-order logic formulas, we develop an automated type inference method for the type system, thereby realizing an automated relatively complete verification of higher-order programs.

Supplementary Material

JPG File (r1d1_talk7.jpg)
MP4 File (r1d1_talk7.mp4)

References

[1]
L. Augustsson. Cayenne - a language with dependent types. In ICFP, pages 239--250, 1998.
[2]
C. Barrett and C. Tinelli. CVC3. In CAV, pages 298--302, 2007.
[3]
E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV, pages 154--169, 2000.
[4]
M. Colón, S. Sankaranarayanan, and H. Sipma. Linear invariant generation using non-linear constraint solving. In CAV, pages 420--432, 2003.
[5]
W. Damm and B. Josko. A sound and relatively_ complete Hoarelogic for a language with higher type procedures. Acta Inf., 20:59--101, 1983.
[6]
S. M. German, E. M. Clarke, and J. Y. Halpern. Reasoning about procedures as parameters. In Logic of Programs, pages 206--220, 1983.
[7]
S. M. German, E. M. Clarke, and J. Y. Halpern. Reasoning about procedures as parameters in the language L4. Inf. Comput., 83(3):265--359, 1989.
[8]
A. Goerdt. A Hoare calculus for functions defined by recursion on higher types. In Logic of Programs, pages 106--117, 1985.
[9]
S. Gulwani, S. Srivastava, and R. Venkatesan. Program analysis as constraint solving. In PLDI, pages 281--292, 2008.
[10]
C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576--580, 1969.
[11]
K. Honda, M. Berger, and N. Yoshida. Descriptive and relative completeness of logics for higher-order functions. In ICALP (2), pages 360--371, 2006.
[12]
R. Jhala and R. Majumdar. Software model checking. ACM Comput. Surv., 41(4), 2009.
[13]
R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: Verifying functional programs using abstract interpreters. In CAV, pages 470--485, 2011.
[14]
R. Jhala and K. L. McMillan. A practical and complete approach to predicate refinement. In TACAS, pages 459--473, 2006.
[15]
T. Johnsson. Lambda lifting: Transforming programs to recursive equations. In FPCA, pages 190--203, 1985.
[16]
N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. In POPL, pages 416--428, 2009.
[17]
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, pages 179--188, 2009.
[18]
N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for higher-order model checking. In PLDI, pages 222--233, 2011.
[19]
U. D. Lago and M. Gaboardi. Linear dependent types and relative completeness. In LICS, pages 133--142, 2011.
[20]
J. Liu, N. Zhan, and H. Zhao. Computing semi-algebraic invariants for polynomial dynamical systems. In EMSOFT, pages 97--106, 2011.
[21]
E.-R. Olderog. Correctness of programs with Pascal-like procedures without global variables. Theor. Comput. Sci., 30:49--90, 1984.
[22]
B. Reus and T. Streicher. Relative completeness for logics of functional programs. In CSL, pages 470--480, 2011.
[23]
P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI, pages 159--169, 2008.
[24]
S. Sankaranarayanan, H. B. Sipma, and Z. Manna. Constraint-based linear-relations analysis. In SAS, pages 53--68, 2004.
[25]
S. Srivastava, S. Gulwani, and J. S. Foster. From program verification to program synthesis. In POPL, pages 313--326, 2010.
[26]
T. Terauchi. Dependent types from counterexamples. In POPL, pages 119--130, 2010.
[27]
H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP, pages 277--288, 2009.
[28]
H. Unno, T. Terauchi, and N. Kobayashi. Automating relatively complete verification of higher-order functional programs, 2012. http://www.kb.is.s.u-tokyo.ac.jp/~uhiro/relcomp.
[29]
A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38--94, 1994.
[30]
H. Xi and F. Pfenning. Dependent types in practical programming. In POPL, pages 214--227, 1999.

Cited By

View all
  • (2024)Answer Refinement Modification: Refinement Type System for Algebraic Effects and HandlersProceedings of the ACM on Programming Languages10.1145/36332808:POPL(115-147)Online publication date: 5-Jan-2024
  • (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
  • (2021)Modelling and verification of parameterized architectures: A functional approachIET Computers & Digital Techniques10.1049/cdt2.1202415:5(335-348)Online publication date: 22-Mar-2021
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2013
    586 pages
    ISBN:9781450318327
    DOI:10.1145/2429069
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: 23 January 2013
Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

  1. higher-order programs
  2. relative completeness
  3. software model checking
  4. type inference

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)13
  • Downloads (Last 6 weeks)3
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Answer Refinement Modification: Refinement Type System for Algebraic Effects and HandlersProceedings of the ACM on Programming Languages10.1145/36332808:POPL(115-147)Online publication date: 5-Jan-2024
  • (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
  • (2021)Modelling and verification of parameterized architectures: A functional approachIET Computers & Digital Techniques10.1049/cdt2.1202415:5(335-348)Online publication date: 22-Mar-2021
  • (2019)HoCHCProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470200(1-14)Online publication date: 24-Jun-2019
  • (2018)ICE-Based Refinement Type Discovery for Higher-Order Functional ProgramsTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-319-89960-2_20(365-384)Online publication date: 12-Apr-2018
  • (2018)Practical Methods for Reasoning About Java 8’s Functional Programming FeaturesVerified Software. Theories, Tools, and Experiments10.1007/978-3-030-03592-1_15(267-278)Online publication date: 18-Jul-2018
  • (2016)Automatically disproving fair termination of higher-order functional programsACM SIGPLAN Notices10.1145/3022670.295191951:9(243-255)Online publication date: 4-Sep-2016
  • (2015)Refinement Type Inference via Horn Constraint OptimizationStatic Analysis10.1007/978-3-662-48288-9_12(199-216)Online publication date: 2-Sep-2015
  • (2015)Inferring Simple Solutions to Recursion-Free Horn Clauses via SamplingProceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 903510.1007/978-3-662-46681-0_10(149-163)Online publication date: 11-Apr-2015
  • (2015)Relaxed Stratification: A New Approach to Practical Complete Predicate RefinementCompiler Construction10.1007/978-3-662-46669-8_25(610-633)Online publication date: 2015
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media