Document Open Access Logo

Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs

Authors Johannes Åman Pohjola, Henrik Rostedt, Magnus O. Myreen

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.32.pdf
  • Filesize: 0.51 MB
  • 19 pages

Document Identifiers

Author Details

Johannes Åman Pohjola
  • Data61/CSIRO, Sydney, Australia, University of New South Wales, Sydney, Australia
Henrik Rostedt
  • Chalmers University of Technology, Gothenburg, Sweden
Magnus O. Myreen
  • Chalmers University of Technology, Gothenburg, Sweden

Funding

  • Åman Pohjola, Johannes: This work was sponsored in part by the U.S. Defense Advanced Research Projects Agency (DARPA). The views expressed are those of the authors and do not reflect the official policy or position of the Defense Advanced Research Projects Agency (DARPA) or the U.S. Government. Approved for Public Release, Distribution Unlimited.
  • Myreen, Magnus O.: This work was supported by the Swedish Foundation for Strategic Research.

Acknowledgements

We are grateful to Robert Sison and the anonymous reviewers for many constructive and insightful comments.

Cite AsGet BibTex

Johannes Åman Pohjola, Henrik Rostedt, and Magnus O. Myreen. Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.32

Abstract

There are useful programs that do not terminate, and yet standard Hoare logics are not able to prove liveness properties about non-terminating programs. This paper shows how a Hoare-like programming logic framework (characteristic formulae) can be extended to enable reasoning about the I/O behaviour of programs that do not terminate. The approach is inspired by transfinite induction rather than coinduction, and does not require non-terminating loops to be productive. This work has been developed in the HOL4 theorem prover and has been integrated into the ecosystem of proof tools surrounding the CakeML programming language.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Software verification
  • Theory of computation → Higher order logic
  • Theory of computation → Separation logic
Keywords
  • Program verification
  • non-termination
  • liveness
  • Hoare logic

Metrics

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

Supplementary Materials

References

  1. Davide Ancona. Soundness of Object-Oriented Languages with Coinductive Big-Step Semantics. In James Noble, editor, Object-Oriented Programming (ECOOP). Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31057-7_21.
  2. Davide Ancona, Francesco Dagnino, and Elena Zucca. Reasoning on divergent computations with coaxioms. PACMPL, 1(OOPSLA), 2017. URL: https://doi.org/10.1145/3133905.
  3. Davide Ancona, Francesco Dagnino, and Elena Zucca. Modeling Infinite Behaviour by Corules. In Object-Oriented Programming (ECOOP), LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2018.21.
  4. Richard Bubel, Crystal Chang Din, Reiner Hähnle, and Keiko Nakata. A Dynamic Logic with Traces and Coinduction. In Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX). Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24312-2_21.
  5. Arthur Charguéraud. Program verification through characteristic formulae. In Paul Hudak and Stephanie Weirich, editors, International Conference on Functional Programming (ICFP). ACM, 2010. Google Scholar
  6. Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In International Conference on Functional Programming (ICFP). ACM, 2011. URL: https://doi.org/10.1145/2034773.2034828.
  7. Arthur Charguéraud. Pretty-Big-Step Semantics. In European Symposium on Programming (ESOP). Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_3.
  8. Arthur Charguéraud. Higher-order representation predicates in separation logic. In Certified Programs and Proofs (CPP), 2016. URL: https://doi.org/10.1145/2854065.2854068.
  9. Arthur Charguéraud and François Pottier. Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation. In Interactive Theorem Proving (ITP), 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_9.
  10. Arthur Charguéraud and François Pottier. Temporary Read-Only Permissions for Separation Logic. In European Symposium on Programming (ESOP). Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_10.
  11. Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter W. O'Hearn. Proving Nontermination via Safety. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2014. URL: https://doi.org/10.1007/978-3-642-54862-8_11.
  12. Hugo Férée, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus O. Myreen, and Son Ho. Program Verification in the Presence of I/O - Semantics, Verified Library Routines, and Verified Applications. In Verified Software: Theories, Tools, Experiments (VSTTE), 2018. URL: https://doi.org/10.1007/978-3-030-03592-1_6.
  13. Roberto Giacobazzi and Isabella Mastroeni. Non-Standard Semantics for Program Slicing. Higher-Order and Symbolic Computation, 16(4), 2003. URL: https://doi.org/10.1023/A:1025872819613.
  14. Armaël Guéneau, Arthur Charguéraud, and François Pottier. A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification. In European Symposium on Programming (ESOP). Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_19.
  15. Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish. Verified Characteristic Formulae for CakeML. In Hongseok Yang, editor, European Symposium on Programming (ESOP), volume 10201 of LNCS. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_22.
  16. Matthew Hennessy and Robin Milner. On Observing Nondeterminism and Concurrency. In J. W. de Bakker and Jan van Leeuwen, editors, Automata, Languages and Programming (ICALP), LNCS. Springer, 1980. URL: https://doi.org/10.1007/3-540-10003-2_79.
  17. Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, and Michael Norrish. Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. In Automated Reasoning - International Joint Conference (IJCAR). Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_42.
  18. Marieke Huisman and Bart Jacobs. Java Program Verification via a Hoare Logic with Abrupt Termination. In Fundamental Approaches to Software Engineering (FASE), 2000. URL: https://doi.org/10.1007/3-540-46428-X_20.
  19. Bart Jacobs and Erik Poll. A Logic for the Java Modeling Language JML. In Fundamental Approaches to Software Engineering (FASE), 2001. URL: https://doi.org/10.1007/3-540-45314-8_21.
  20. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Transfinite Reductions in Orthogonal Term Rewriting Systems. Inf. Comput., 119(1), 1995. URL: https://doi.org/10.1006/inco.1995.1075.
  21. Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: formal verification of an operating-system kernel. Commun. ACM, 53(6), 2010. URL: https://doi.org/10.1145/1743546.1743574.
  22. Ihor Kuz, Yan Liu, Ian Gorton, and Gernot Heiser. CAmkES: A component model for secure microkernel-based embedded systems. Journal of Systems and Software, 80(5), 2007. URL: https://doi.org/10.1016/j.jss.2006.08.039.
  23. Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, and Wei-Ngan Chin. A Resource-Based Logic for Termination and Non-termination Proofs. In International Conference on Formal Engineering Methods (ICFEM), 2014. URL: https://doi.org/10.1007/978-3-319-11737-9_18.
  24. Ton Chanh Le, Shengchao Qin, and Wei-Ngan Chin. Termination and non-termination specification inference. In Programming Language Design and Implementation (PLDI). ACM, 2015. URL: https://doi.org/10.1145/2737924.2737993.
  25. Xavier Leroy. A Formally Verified Compiler Back-end. J. Autom. Reasoning, 43(4), 2009. URL: https://doi.org/10.1007/s10817-009-9155-4.
  26. Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Inf. Comput., 207(2), 2009. URL: https://doi.org/10.1016/j.ic.2007.12.004.
  27. Keiko Nakata and Tarmo Uustalu. Trace-Based Coinductive Operational Semantics for While. In Theorem Proving in Higher Order Logics (TPHOLs). Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_26.
  28. Keiko Nakata and Tarmo Uustalu. A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While. In European Symposium on Programming (ESOP). Springer, 2010. URL: https://doi.org/10.1007/978-3-642-11957-6_26.
  29. Keiko Nakata and Tarmo Uustalu. Resumptions, Weak Bisimilarity and Big-Step Semantics for While with Interactive I/O: An Exercise in Mixed Induction-Coinduction. In Structural Operational Semantics (SOS), 2010. URL: https://doi.org/10.4204/EPTCS.32.5.
  30. Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. Functional Big-Step Semantics. In Peter Thiemann, editor, European Symposium on Programming (ESOP), LNCS. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_23.
  31. Willem Penninckx, Bart Jacobs, and Frank Piessens. Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs. In European Symposium on Programming (ESOP). Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46669-8_7.
  32. Casper Bach Poulsen and Peter D. Mosses. Flag-based big-step semantics. J. Log. Algebr. Meth. Program., 88, 2017. URL: https://doi.org/10.1016/j.jlamp.2016.05.001.
  33. Davide Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5), October 1998. URL: https://doi.org/10.1017/S0960129598002527.
  34. Dana Scott and J.W. De Bakker. A Theory of Programs. Unpublished manuscript, IBM Vienna, 1969. Google Scholar
  35. Konrad Slind, David S. Hardin, Johannes Åman Pohjola, and Michael Sproul. Synthesis of Verified Architectural Components for Autonomy Hosted on a Verified Microkernel. Draft, 2019. Google Scholar
  36. Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. The verified CakeML compiler backend. Journal of Functional Programming, 29, 2019. URL: https://doi.org/10.1017/S0956796818000229.
  37. D. A. Turner. Total Functional Programming. J. UCS, 10(7), 2004. URL: https://doi.org/10.3217/jucs-010-07-0751.
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