Document Open Access Logo

REST: Integrating Term Rewriting with Program Verification

Authors Zachary Grannan , Niki Vazou , Eva Darulova , Alexander J. Summers

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.13.pdf
  • Filesize: 1.17 MB
  • 29 pages

Document Identifiers

Author Details

Zachary Grannan
  • University of British Columbia, Vancouver, Canada
Niki Vazou
  • IMDEA Software Institute, Madrid, Spain
Eva Darulova
  • Uppsala University, Sweden
Alexander J. Summers
  • University of British Columbia, Vancouver, Canada

Funding

This work was supported by the Juan de la Cierva grants IJC2019-041599-I, the HaCrypt ONR project N00014-19-1-2292, and the ERC starting grant CRETE (101039196). We acknowledge the support of the Natural Sciences and Engineering Research Council of Canada (NSERC).

Acknowledgements

We thank Jonathan Chan, Eric Conlon, Rui Ge, Paulette Koronkevich and the anonymous reviewers for their helpful and constructive feedback.

Cite AsGet BibTex

Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers. REST: Integrating Term Rewriting with Program Verification. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 13:1-13:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.13

Abstract

We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables flexible but terminating term rewriting for theorem proving by: (1) exploiting newly-introduced term orderings that are more permissive than standard rewrite simplification orderings; (2) dynamically and iteratively selecting orderings based on the path of rewrites taken so far; and (3) integrating external oracles that allow steps that cannot be justified with rewrite rules. Our REST approach is designed around an easily implementable core algorithm, parameterizable by choices of term orderings and their implementations; in this way our approach can be easily integrated into existing tools. We implemented REST as a Haskell library and incorporated it into Liquid Haskell’s evaluation strategy, extending Liquid Haskell with rewriting rules. We evaluated our REST implementation by comparing it against both existing rewriting techniques and E-matching (as used in most SMT solvers) and by showing that it can be used to supplant manual lemma application in many existing Liquid Haskell proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • term rewriting
  • program verification
  • theorem proving

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Agda Developers. The Agda Language Reference, version 2.6.1, 2020. Available electronically at URL: https://agda.readthedocs.io/en/v2.6.1/language/index.html.
  2. Nada Amin, K Rustan M Leino, and Tiark Rompf. Computing with an smt solver. In International Conference on Tests and Proofs, pages 20-35. Springer, 2014. Google Scholar
  3. Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236(1):133-178, April 2000. URL: https://doi.org/10.1016/S0304-3975(99)00207-8.
  4. Jeremy Avigad, Leonardo de Moura, and Soonho Kong. Theorem Proving in Lean, Release 3.20.0, September 2020. p 73. URL: https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf.
  5. Jeremy Avigad, Gabriel Ebner, and Sebastian Ullrich. The Lean Reference Manual, Release 3.3.0, 2018. URL: https://leanprover.github.io/reference/lean_reference.pdf.
  6. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi'c, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV '11), volume 6806 of Lecture Notes in Computer Science, pages 171-177. Springer, July 2011. Snowbird, Utah. URL: http://www.cs.stanford.edu/~barrett/pubs/BCD+11.pdf.
  7. N. Becker, P. Müller, and A. J. Summers. The axiom profiler: Understanding and debugging smt quantifier instantiations. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2019, LNCS, pages 99-116. Springer-Verlag, 2019. Google Scholar
  8. Maximilian Bolingbroke and Simon Peyton Jones. Supercompilation by evaluation. SIGPLAN Not., 45(11):135-146, September 2010. URL: https://doi.org/10.1145/2088456.1863540.
  9. Maximilian Bolingbroke, Simon Peyton Jones, and Dimitrios Vytiniotis. Termination combinators forever. In Proceedings of the 4th ACM symposium on Haskell, pages 23-34, 2011. Google Scholar
  10. Joachim Breitner. A promise checked is a promise kept: inspection testing. In Nicolas Wu, editor, Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2018, St. Louis, MO, USA, September 27-17, 2018, pages 14-25. ACM, 2018. URL: https://doi.org/10.1145/3242744.3242748.
  11. The Coq Development Team. The Coq Reference Manual, version 8.11.2, 2020. Available electronically at URL: http://coq.inria.fr/refman.
  12. Leonardo de Moura and Nikolaj Bjørner. Efficient e-matching for smt solvers. In Frank Pfenning, editor, Automated Deduction - CADE-21, pages 183-198, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  13. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In International conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. Google Scholar
  14. Nachum Dershowitz. A note on simplification orderings. Information Processing Letters, 9(5):212-215, 1979. URL: https://doi.org/10.1016/0020-0190(79)90071-1.
  15. Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical computer science, 17(3):279-301, 1982. Google Scholar
  16. Nachum Dershowitz. Termination of rewriting. Journal of symbolic computation, 3(1-2):69-115, 1987. Google Scholar
  17. Nachum Dershowitz, Jieh Hsiang, N Alan Josephson, and David A Plaisted. Associative-commutative rewriting. In IJCAI, pages 940-944, 1983. Google Scholar
  18. Nachum Dershowitz and Zohar Manna. Proving termination with multiset orderings. In Hermann A. Maurer, editor, Automata, Languages and Programming, Lecture Notes in Computer Science, pages 188-202, Berlin, Heidelberg, 1979. Springer. URL: https://doi.org/10.1007/3-540-09510-1_15.
  19. David Detlefs, Greg Nelson, and James B. Saxe. Simplify: A theorem prover for program checking. J. ACM, 52(3):365-473, May 2005. URL: https://doi.org/10.1145/1066100.1066102.
  20. David Detlefs, Greg Nelson, and James B Saxe. Simplify: a theorem prover for program checking. Journal of the ACM (JACM), 52(3):365-473, 2005. Google Scholar
  21. Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. Adding decision procedures to smt solvers using axioms with triggers. Journal of Automated Reasoning, 56(4):387-457, 2016. Google Scholar
  22. Andrew Farmer, Neil Sculthorpe, and Andy Gill. Reasoning with the hermit: Tool support for equational reasoning on ghc core programs. In Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell, Haskell ’15, pages 23-34, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2804302.2804303.
  23. Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, Programming Languages and Systems (ESOP), volume 7792 of Lecture Notes in Computer Science, pages 125-128. Springer, 2013. Google Scholar
  24. Jürgen Giesl, Cornelius Aschermann, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Jera Hensel, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, et al. Analyzing program termination and complexity automatically with aprove. Journal of Automated Reasoning, 58(1):3-31, 2017. Google Scholar
  25. Zachary Grannan. rest-rewrite: Rewriting library with online termination checking, 2022. URL: https://hackage.haskell.org/package/rest-rewrite.
  26. Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers. Rest: Integrating term rewriting with program verification (extended version), 2022. URL: http://arxiv.org/abs/2202.05872.
  27. Jieh Hsiang, Hélène Kirchner, Pierre Lescanne, and Michaël Rusinowitch. The term rewriting approach to automated theorem proving. The Journal of Logic Programming, 14(1):71-99, October 1992. URL: https://doi.org/10.1016/0743-1066(92)90047-7.
  28. Gerard Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS '77, pages 30-45, USA, 1977. IEEE Computer Society. URL: https://doi.org/10.1109/SFCS.1977.9.
  29. OEIS Foundation Inc. The On-Line Encyclopedia of Integer Sequences, 2022. A000798: Number of different quasi-orders (or topologies, or transitive digraphs) with n labeled elements. URL: https://oeis.org/A000798.
  30. J. W. Klop. Term Rewriting Systems, pages 1-116. Oxford University Press, Inc., USA, 1993. Google Scholar
  31. Donald E Knuth and Peter B Bendix. Simple word problems in universal algebras. In Automation of Reasoning, pages 342-376. Springer, 1983. Google Scholar
  32. Joseph B Kruskal. The theory of well-quasi-ordering: A frequently discovered concept. Journal of Combinatorial Theory, Series A, 13(3):297-305, November 1972. URL: https://doi.org/10.1016/0097-3165(72)90063-5.
  33. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’01, pages 81-92, New York, NY, USA, 2001. Association for Computing Machinery. URL: https://doi.org/10.1145/360204.360210.
  34. K. R. M. Leino and Clément Pit-Claudel. Trigger Selection Strategies to Stabilize Program Verifiers. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification, Lecture Notes in Computer Science, pages 361-381, Cham, 2016. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-41528-4_20.
  35. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’10, pages 348-370, Berlin, Heidelberg, 2010. Springer-Verlag. Google Scholar
  36. K Rustan M Leino and Nadia Polikarpova. Verified calculations. In Working Conference on Verified Software: Theories, Tools, and Experiments, pages 170-190. Springer, 2013. Google Scholar
  37. Michael Leuschel. Homeomorphic Embedding for Online Termination of Symbolic Methods. In Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Torben Æ. Mogensen, David A. Schmidt, and I. Hal Sudborough, editors, The Essence of Computation, volume 2566, pages 379-403. Springer Berlin Heidelberg, Berlin, Heidelberg, 2002. Series Title: Lecture Notes in Computer Science. URL: https://doi.org/10.1007/3-540-36377-7_17.
  38. Jia Meng and Lawrence C Paulson. Translating higher-order clauses to first-order clauses. Journal of Automated Reasoning, 40(1):35-60, 2008. Google Scholar
  39. P. Müller, M. Schwerhoff, and A. J. Summers. Viper: A verification infrastructure for permission-based reasoning. In VMCAI, 2016. Google Scholar
  40. Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, 2020. Google Scholar
  41. Ulf Norell. Dependently typed programming in agda. In Proceedings of the 6th International Conference on Advanced Functional Programming, AFP’08, pages 230-266, Berlin, Heidelberg, 2008. Springer-Verlag. Google Scholar
  42. Andres Nötzli, Andrew Reynolds, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Clark Barrett, and Cesare Tinelli. Syntax-guided rewrite rule enumeration for smt solvers. In Mikoláš Janota and Inês Lynce, editors, Theory and Applications of Satisfiability Testing - SAT 2019, pages 279-297, Cham, 2019. Springer International Publishing. Google Scholar
  43. Lawrence C Paulson and Kong Woei Susanto. Source-level proof reconstruction for interactive theorem proving. In International Conference on Theorem Proving in Higher Order Logics, pages 232-245. Springer, 2007. Google Scholar
  44. Lawrence C Paulsson and Jasmin C Blanchette. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Proceedings of the 8th International Workshop on the Implementation of Logics (IWIL-2010), Yogyakarta, Indonesia. EPiC, volume 2, 2012. Google Scholar
  45. Julien Signoles, Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, and Boris Yakobowski. Frama-c: a software analysis perspective. Formal Aspects of Computing, 27, October 2012. URL: https://doi.org/10.1007/s00165-014-0326-7.
  46. William Sonnex, Sophia Drossopoulou, and Susan Eisenbach. Zeno: An automated prover for properties of recursive data structures. In Cormac Flanagan and Barbara König, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 407-421, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. Google Scholar
  47. Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. Dependent types and multi-monadic effects in F*. In 43rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 256-270. ACM, January 2016. URL: https://www.fstar-lang.org/papers/mumon/.
  48. Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. Equality saturation: a new approach to optimization. In POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pages 264-276, New York, NY, USA, 2009. ACM. URL: https://doi.org/10.1145/1480881.1480915.
  49. René Thiemann and Jürgen Giesl. Size-Change Termination for Term Rewriting. In Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings, volume 2706, pages 264-278, March 2007. URL: https://doi.org/10.1007/3-540-44881-0_19.
  50. Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, and Graham Hutton. Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). In Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, Haskell 2018, pages 132-144, St. Louis, MO, USA, September 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3242744.3242756.
  51. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. Refinement types for haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP ’14, pages 269-282, New York, NY, USA, 2014. Association for Computing Machinery. URL: https://doi.org/10.1145/2628136.2628161.
  52. Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. Refinement reflection: Complete verification with smt. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158141.
  53. Dimitrios Vytiniotis, Simon Peyton Jones, Koen Claessen, and Dan Rosén. Halo: Haskell to logic through denotational semantics. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 431-442, 2013. Google Scholar
  54. Philip Wadler. Deforestation: transforming programs to eliminate trees. Theoretical Computer Science, 73(2):231-248, 1990. URL: https://doi.org/10.1016/0304-3975(90)90147-A.
  55. Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. Egg: Fast and extensible equality saturation. Proceedings of the ACM on Programming Languages, 5(POPL):1-29, 2021. Google Scholar
  56. Akihisa Yamada, Keiichirou Kusakari, and Toshiki Sakabe. Nagoya termination tool. In Rewriting and Typed Lambda Calculi, pages 466-475. Springer, 2014. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact