research-article

Open access

Higher-order constrained horn clauses for verification

Authors:

Toby Cathcart Burn,

C.-H. Luke Ong,

Steven J. RamsayAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL

Article No.: 11, Pages 1 - 28

https://doi.org/10.1145/3158099

Published: 27 December 2017 Publication History

Abstract

Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision problem concerning their satisfiability. We show that, although satisfiable systems of higher-order clauses do not generally have least models, there is a notion of canonical model obtained through a reduction to a problem concerning a kind of monotone logic program. Following work in higher-order program verification, we develop a refinement type system in order to reason about and automate the search for models. This provides a sound but incomplete method for solving the decision problem. Finally, we show that there is a sense in which we can use refinement types to express properties of terms whilst staying within the higher-order constrained Horn clause framework.

Supplementary Material

WEBM File (higherorderconstrainedhorn.webm)

Download
130.08 MB

References

[1]

Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. 2013. Solving Existentially Quantified Horn Clauses. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. 869–882.

Digital Library

[2]

Per Bjesse, Koen Claessen, Mary Sheeran, and Satnam Singh. 1998. Lava: Hardware Design in Haskell. In Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP ’98), Baltimore, Maryland, USA, September 27-29, 1998. 174–184.

Digital Library

[3]

Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. 2015. Horn Clause Solvers for Program Verification. In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday. 24–51.

[4]

Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko. 2012. Program Verification as Satisfiability Modulo Theories. In 10th International Workshop on Satisfiability Modulo Theories, SMT 2012, Manchester, UK, June 30 - July 1, 2012. 3–11.

[5]

Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko. 2013a. Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types. CoRR abs/1306.5264 (2013).

[6]

Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko. 2013b. On Solving Universally Quantified Horn Clauses. In Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. 105–125.

[7]

Andreas Blass and Yuri Gurevich. 1987. Computation Theory and Logic. Springer-Verlag, London, UK, UK, Chapter Existential Fixed-point Logic, 20–36.

[8]

Christopher H. Broadbent, Arnaud Carayol, Matthew Hague, and Olivier Serre. 2013. C-SHORe: a collapsible approach to verifying higher-order programs. In International Conference on Functional Programming, ICFP’13. ACM, 13–24.

Digital Library

[9]

Christopher H. Broadbent and Naoki Kobayashi. 2013. Saturation-based model checking of higher-order recursion schemes. In Computer Science Logic, CSL’13 (LIPIcs), Vol. 23. Schloss Dagstuhl – Leibniz-Zentrum fuer Informatik, 129–148.

[10]

Angelos Charalambidis, Zoltán Ésik, and Panos Rondogiannis. 2014. Minimum Model Semantics for Extensional Higher-order Logic Programming with Negation. TPLP 14, 4-5 (2014), 725–737.

[11]

Angelos Charalambidis, Konstantinos Handjopoulos, Panagiotis Rondogiannis, and William W. Wadge. 2013. Extensional Higher-Order Logic Programming. ACM Trans. Comput. Log. 14, 3 (2013), 21.

Digital Library

[12]

Weidong Chen, Michael Kifer, and David S. Warren. 1993. HiLog: A foundation for higher-order logic programming. Journal of Logic Programming 15, 3 (1993), 187–230.

Digital Library

[13]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TA-CAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg, 337–340.

[14]

Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. 2012. HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings. 549–551.

[15]

Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. 343–361.

[16]

Nevin Heintze. 1995. Control-Flow Analysis and Type Systems. In Proceedings of the Static Analysis Symposium, SAS’95 (Lecture Notes in Computer Science). Springer, 189–206.

[17]

Nevin Heintze, Spiro Michaylov, and Peter Stuckey. 1992. CLP(âĎIJ) and some electrical engineering problems. Journal of Automated Reasoning 9, 2 (1992), 231–260.

Digital Library

[18]

Krystof Hoder, Nikolaj Bjørner, and Leonardo Mendonça de Moura. 2011. µZ- An Efficient Engine for Fixed Points with Constraints. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. 457–462.

[19]

Joxan Jaffar and Michael J. Maher. 1994. Constraint Logic Programming: A Survey. J. Log. Program. 19/20 (1994), 503–581.

[20]

Ranjit Jhala, Rupak Majumdar, and Andrey Rybalchenko. 2011. HMC: Verifying Functional Programs Using Abstract Interpreters. In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. 470–485.

Digital Library

[21]

Naoki Kobayashi. 2013. Model Checking Higher-Order Programs. J. ACM 60, 3 (2013), 20:1–20:62.

Digital Library

[22]

Naoki Kobayashi and C.-H. Luke Ong. 2009. A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. In Logic in Computer Science, LICS 2009. IEEE Computer Society, 179–188.

Digital Library

[23]

Naoki Kobayashi, Ryosuke Sato, and Hiroshi Unno. 2011. Predicate abstraction and CEGAR for higher-order model checking. In Programming Languages Design and Implementation, PLDI’11. ACM, 222–233.

Digital Library

[24]

James Lipton and Susana Nieva. 2007. Higher-Order Logic Programming Languages with Constraints: A Semantics. In Typed Lambda Calculi and Applications: 8th International Conference, TLCA 2007, Paris, France,June 26-28, 2007. Proceedings, Simona Ronchi Della Rocca (Ed.). Springer Berlin Heidelberg.

[25]

Saunders Mac Lane. 1971. Categories for the Working Mathematician. Springer.

[26]

Gopalan Nadathur and Dale Miller. 1990. Higher-Order Horn Clauses. J. ACM 37, 4 (1990), 777–814.

Digital Library

[27]

C.-H. Luke Ong. 2006. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In Logic In Computer Science, LICS’06. IEEE Computer Society, 81–90.

[28]

Jens Palsberg. 1998. Equality-based flow analysis versus recursive types. ACM Trans. Program. Lang. Syst. 20, 6 (1998), 1251–1264.

Digital Library

[29]

Steven J. Ramsay, Robin P. Neatherway, and C.-H. Luke Ong. 2014. A Type-Directed Abstraction Refinement Approach to Higher-Order Model Checking. In Principles of Programming Languages, POPL’14. ACM, 61–72.

Digital Library

[30]

John C. Reynolds. 1972. Definitional Interpreters for Higher-order Programming Languages. In Proceedings of the ACM Annual Conference - Volume 2 (ACM ’72). 717–740.

Digital Library

[31]

Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid types. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008. 159–169.

Digital Library

[32]

Tachio Terauchi. 2010. Dependent types from counterexamples. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. 119–130.

Digital Library

[33]

Hiroshi Unno and Naoki Kobayashi. 2009. Dependent type inference with interpolants. In Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal. 277–288.

Digital Library

[34]

Hiroshi Unno, Tachio Terauchi, and Naoki Kobayashi. 2013. Automating Relatively Complete Verification of Higher-order Functional Programs. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’13). ACM, New York, NY, USA, 75–86.

Digital Library

[35]

Niki Vazou, Alexander Bakst, and Ranjit Jhala. 2015. Bounded refinement types. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015. 48–61.

Digital Library

[36]

Niki Vazou, Patrick Maxim Rondon, and Ranjit Jhala. 2013. Abstract Refinement Types. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. 209–228.

Digital Library

[37]

Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement Types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). 269–282.

Digital Library

[38]

William W. Wadge. 1991. Higher-Order Horn Logic Programming. In Logic Programming, Proceedings of the 1991 International Symposium, San Diego, California, USA, Oct. 28 - Nov 1, 1991. 289–303.

[39]

He Zhu and Suresh Jagannathan. 2013. Compositional and Lightweight Dependent Type Inference for ML. In Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings. 295–314.

Digital Library

Cited By

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
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
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
Show More Cited By

Index Terms

Higher-order constrained horn clauses for verification
1. Theory of computation
  1. Logic
    1. Logic and verification
  2. Semantics and reasoning
    1. Program constructs
      1. Functional constructs
    2. Program reasoning
      1. Program verification

Recommendations

Higher Order Horn Clauses
Higher-Order Horn Clauses
Higher-order Horn clauses

A generalization of Horn clauses to a higher-order logic is described and examined as a basis for logic programming. In qualitative terms, these higher-order Horn clauses are obtained from the first-order ones by replacing first-order terms with simply ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Artifacts Evaluated & Functional

Author Tags

Qualifiers

Research-article

Funding Sources

Engineering and Physical Sciences Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
1,160
Total Downloads

Downloads (Last 12 months)141
Downloads (Last 6 weeks)17

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

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
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
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
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
Asada KKatsura HKobayashi N(2022)On Higher-Order Reachability Games Vs May ReachabilityReachability Problems10.1007/978-3-031-19135-0_8(108-124)Online publication date: 12-Oct-2022
https://doi.org/10.1007/978-3-031-19135-0_8
Jochems J(2021)Reducing Higher-order Recursion Scheme Equivalence to Coinductive Higher-order Constrained Horn ClausesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.344.4344(36-64)Online publication date: 13-Sep-2021
https://doi.org/10.4204/EPTCS.344.4
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
Matsushita YTsukada TKobayashi N(2021)RustHorn: CHC-based Verification for Rust ProgramsACM Transactions on Programming Languages and Systems10.1145/346220543:4(1-54)Online publication date: 31-Oct-2021
https://dl.acm.org/doi/10.1145/3462205
Jones ERamsay S(2021)Intensional datatype refinement: with application to scalable verification of pattern-match safetyProceedings of the ACM on Programming Languages10.1145/34343365:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434336
Kenyon-Roberts AOng CGorla D(2021)Supermartingales, ranking functions and probabilistic lambda calculusProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470550(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470550
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents