UTC Time, Formally Verified
Authors: 
Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez, Eduardo Hermo Reyes, Joaquim Casals Buñuel, Joost JoostenAuthors Info & Claims
Pages 2 - 13
Abstract
FV Time is a small-scale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds, which are part of the UTC standard but usually not implemented in existing libraries. Since the verified functions of FV Time are reasonably simple yet non-trivial, it nicely illustrates our methodology for verifying software with Coq.
In this paper we present a description of the project, emphasizing the main problems faced while developing the library, as well as some general-purpose solutions that were produced as by-products and may be used in other verification projects. These include a refinement package between proof-oriented MathComp numbers and computation-oriented primitive numbers from the Coq standard library, as well as a set of tactics to automatically prove certain decidable statements over finite ranges through brute-force computation.
References
[1]
Ana de Almeida Borges. 2022. Towards a Coq formalization of a quantified modal logic. In Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022), Christoph Benzmüller and Jens Otten (Eds.). CEUR, Haifa, Israel, 13–27. https://ceur-ws.org/Vol-3326/ARQNL2022_paper1.pdf
[2]
Ana de Almeida Borges, Joaquim Casals Buñuel, Juan Conejero Rodríguez, Mireia González Bedmar, and Eduardo Hermo Reyes. 2023. The FormalV Library. Version 1.2.0.
[3]
Ana de Almeida Borges, Juan Conejero Rodríguez, David Fernández-Duque, Mireia González Bedmar, and Joost J. Joosten. 2021. To drive or not to drive: A logical and computational analysis of European transport regulations. Information and Computation 280 (2021), 104636. issn:0890-5401
[4]
Ana de Almeida Borges, Guillaume Melquiond, and Pierre Roux. 2021. Signed primitive integers. https://github.com/coq/coq/pull/13559
[5]
Android. 2022. Date Class. Android Reference Manual. https://developer.android.com/reference/java/util/Date
[6]
Andrew W. Appel. 2011. Verified Software Toolchain. In Programming Languages and Systems, Gilles Barthe (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1–17. isbn:978-3-642-19718-5
[7]
Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Trans. Program. Lang. Syst. 37, 2, Article 7 (2015), 31 pages. issn:0164-0925
[8]
Andrew W Appel. 2022. Coq’s vibrant ecosystem for verification engineering (invited talk). In Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM, New York, NY, United States, 2–11.
[9]
R.J.R. Back. 1981. On correct refinement of programs. J. Comput. System Sci. 23, 1 (1981), 49–68. issn:0022-0000
[10]
Frédéric Besson. 2007. Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. In Types for Proofs and Programs, Thorsten Altenkirch and Conor McBride (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 48–62. isbn:978-3-540-74464-1
[11]
Frédéric Besson. 2021. Itauto: An Extensible Intuitionistic SAT Solver. In 12th International Conference on Interactive Theorem Proving (ITP 2021) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 193), Liron Cohen and Cezary Kaliszyk (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 9:1–9:18. isbn:978-3-95977-188-7 issn:1868-8969
[12]
Dominique Cansell, J. Paul Gibson, and Dominique Méry. 2007. Refinement: A Constructive Approach to Formal Software Design for a Secure e-voting Interface. Electronic Notes in Theoretical Computer Science 183 (2007), 39–55. issn:1571-0661 Proceedings of the First International Workshop on Formal Methods for Interactive Systems (FMIS 2006).
[13]
Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2015. Using Crash Hoare Logic for Certifying the FSCQ File System. In Proceedings of the 25th Symposium on Operating Systems Principles (Monterey, California) (SOSP ’15). Association for Computing Machinery, New York, NY, USA, 18–37. isbn:9781450338349
[14]
Adam Chlipala. 2010. A Verified Compiler for an Impure Functional Language. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Madrid, Spain) (POPL ’10). Association for Computing Machinery, New York, NY, USA, 93–106. isbn:9781605584799
[15]
Adam Chlipala. 2011. Mostly-Automated Verification of Low-Level Programs in Computational Separation Logic. SIGPLAN Not. 46, 6 (jun 2011), 234–245. issn:0362-1340
[16]
Cyril Cohen, Maxime Dénès, and Anders Mörtberg. 2013. Refinements for Free!. In Certified Programs and Proofs (Lecture Notes in Computer Science, Vol. 8307), Georges Gonthier and Michael Norrish (Eds.). Springer, Cham, 147–162.
[17]
Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. 2020. Hierarchy Builder: Algebraic hierarchies made easy in Coq with Elpi. In FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction (5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), 167), Zena M. Ariola (Ed.). Schloss Dagstuhl, Paris, France, 34:1–34:21.
[18]
Comité international des poids et mesures. 2022. Resolutions of the General Conference on Weights and Measures (27th meeting). https://www.bipm.org/documents/20126/77765681/Resolutions-2022.pdf/281f3160-fc56-3e63-dbf7-77b76500990f
[19]
Ernesto Copello, Nora Szasz, and Álvaro Tasistro. 2018. Machine-checked Proof of the Church-Rosser Theorem for the Lambda Calculus Using the Barendregt Variable Convention in Constructive Type Theory. Electronic Notes in Theoretical Computer Science 338 (2018), 79–95. issn:1571-0661 The 12th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2017).
[20]
Coq Development Team. 2023. Coq.ssr.ssreflect. Coq Standard Library Version 8.17.1. https://coq.inria.fr/doc/V8.17.1/stdlib/Coq.ssr.ssreflect.html
[21]
Coq Development Team. 2023. Programmable proof search. Coq Reference Manual Version 8.17.1. https://coq.github.io/doc/v8.17/refman/proofs/automatic-tactics/auto.html
[22]
Pierre Corbineau. 2004. First-Order Reasoning in the Calculus of Inductive Constructions. In Types for Proofs and Programs, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 162–177. isbn:978-3-540-24849-1
[23]
cppreference.com Team. 2021. utc_clock. C++ Reference Manual. https://en.cppreference.com/mwiki/index.php?title=cpp/chrono/utc_clock&oldid=134878
[24]
Łukasz Czajka. 2020. Practical Proof Search for Coq by Type Inhabitation. In Automated Reasoning, Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer International Publishing, Cham, 28–57. isbn:978-3-030-51054-1
[25]
Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. 2015. Fiat: Deductive synthesis of abstract data types in a proof assistant. ACM SIGPLAN Notices 50, 1 (2015), 689–700.
[26]
William DeMeo. 2022. The Agda Universal Algebra Library. http://ualib.org/
[27]
Maxime Dénès, Anders Mörtberg, and Vincent Siles. 2012. A Refinement-Based Approach to Computational Algebra in Coq. In ITP 2012: Interactive Theorem Proving (Lecture Notes in Computer Science, Vol. 7406), Lennart Beringer and Amy Felty (Eds.). Springer, Berlin, Heidelberg, 83–98.
[28]
European Parliament and Council of the European Union. 2016. COMMISSION IMPLEMENTING REGULATION (EU) 2016/799 of 18 March 2016 implementing Regulation (EU) No 165/2014 of the European Parliament and of the Council laying down the requirements for the construction, testing, installation, operation and repair of tachographs and their components. Official Journal of the European Union. https://eur-lex.europa.eu/legal-content/EN/TXT/?uri=CELEX
[29]
Formal Vindications S.L. 2022. How-To: Use of the FV Time Manager on Windows, Linux and other platforms through its command line interface. https://formalv.gitlab.io/fv-docs/fvtm-tech-spec.pdf
[30]
Yannick Forster, Dominik Kirst, and Gert Smolka. 2019. On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (Cascais, Portugal) (CPP 2019). Association for Computing Machinery, New York, NY, USA, 38–51. isbn:9781450362221
[31]
Georges Gonthier. 2008. Formal proof – the four-color theorem. Notices of the American Mathematical Society 55, 11 (2008), 1382–1393.
[32]
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. 2013. A Machine-Checked Proof of the odd order theorem. In Interactive Theorem Proving, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 163–179.
[33]
Mireia González Bedmar. 2022. A method for clean extraction: example. https://gitlab.com/formalv/extraction-model
[34]
Google. 2022. Unsmear. https://github.com/google/unsmear
[35]
Benjamin Grégoire and Xavier Leroy. 2002. A compiled implementation of strong reduction. In Proceedings of the seventh ACM SIGPLAN international conference on Functional programming. ACM, New York, NY, United States, 235–246.
[36]
Benjamin Grégoire and Assia Mahboubi. 2005. Proving Equalities in a Commutative Ring Done Right in Coq. In Theorem Proving in Higher Order Logics, Joe Hurd and Tom Melham (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 98–113. isbn:978-3-540-31820-0
[37]
Florian Haftmann, Alexander Krauss, Ondřej Kunčar, and Tobias Nipkow. 2013. Data Refinement in Isabelle/HOL. In Interactive Theorem Proving, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 100–115. isbn:978-3-642-39634-2
[38]
John Harrison. 1999. A Machine-Checked Theory of Floating Point Arithmetic. In Theorem Proving in Higher Order Logics, Yves Bertot, Gilles Dowek, Laurent Théry, André Hirschowitz, and Christine Paulin (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 113–130. isbn:978-3-540-48256-7
[39]
Howard Hinnant. 2019. chrono-Compatible Low-Level Date Algorithms. https://howardhinnant.github.io/date_algorithms.html
[40]
IEEE and The Open Group. 2018. The Open Group Base Specifications Issue 7. https://pubs.opengroup.org/onlinepubs/9699919799/
[41]
IETF. 2016. Leap seconds list. https://www.ietf.org/timezones/data/leap-seconds.list
[42]
ITU Radiocommunication Assembly. 2002. Recommendation ITU-R TF.460-6: Standard-frequency and time-signal emissions. International Telecommunication Union (2002). https://www.itu.int/dms_pubrec/itu-r/rec/tf/R-REC-TF.460-6-200202-I!!PDF-E.pdf
[43]
Daan Leijen. 2016. UTC time calculation. The Koka Programming Language Documentation. https://koka-lang.github.io/koka/doc/std_time_utc.html
[44]
Xavier Leroy. 2009. Formal Verification of a Realistic Compiler. Commun. ACM 52, 7 (Jul 2009), 107–115. issn:0001-0782
[45]
Pierre Letouzey. 2003. A New Extraction for Coq. In Types for Proofs and Programs, Herman Geuvers and Freek Wiedijk (Eds.). Springer, Berlin, Heidelberg, 200–219. isbn:978-3-540-39185-2
[46]
Pierre Letouzey. 2004. Programmation fonctionnelle certifiée: l’extraction de programmes dans l’assistant Coq. Ph. D. Dissertation. Université Paris Sud-Paris XI.
[47]
Pierre Letouzey. 2008. Extraction in Coq: An overview. In Logic and Theory of Algorithms, Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe (Eds.). Springer, Springer Berlin Heidelberg, Berlin, Heidelberg, 359–369.
[48]
Judah Levine, Patrizia Tavella, and Martin Milton. 2023. Towards a consensus on a continuous coordinated universal time. Metrologia 60, 1 (2023), 014001.
[49]
Assia Mahboubi. 2013. The rooster and the butterflies. In International Conference on Intelligent Computer Mathematics. Springer-Verlag, Berlin, Heidelberg, 1–18.
[50]
Mathematical Components Team. 2007. The Mathematical Components library. https://math-comp.github.io/
[51]
MathWorks. 2022. leapseconds. MATLAB Reference Manual. https://www.mathworks.com/help/matlab/ref/leapseconds.html
[52]
Guillaume Melquiond. 2023. Coq Interval. https://coqinterval.gitlabpages.inria.fr/
[53]
Microsoft. 2022. DateTime.Ticks. Microsoft .NET 6 Documentation. https://docs.microsoft.com/en-us/dotnet/api/system.datetime.ticks?view=net-6.0
[54]
Kazuhiko Sakaguchi. 2020. Validating Mathematical Structures. In Automated Reasoning, Nicolas Peltier and Viorica Sofronie-Stokkermans (Eds.). Springer International Publishing, Cham, 138–157.
[55]
Kazuhiko Sakaguchi. 2021. Mczify. https://github.com/math-comp/mczify
[56]
Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, and Théo Winterhalter. 2023. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. (2023). https://inria.hal.science/hal-04077552 hal-04077552.
Index Terms
- UTC Time, Formally Verified
Index terms have been assigned to the content through auto-classification.
Recommendations
Verdi: a framework for implementing and formally verifying distributed systems
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and ImplementationDistributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex ...
Verdi: a framework for implementing and formally verifying distributed systems
PLDI '15Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex ...
A Formally Verified Cut-Elimination Procedure for Linear Nested Sequents for Tense Logic
Automated Reasoning with Analytic Tableaux and Related MethodsAbstractWe port Dawson and Goré’s general framework of deep embeddings of derivability from Isabelle to Coq. By using lists instead of multisets to encode sequents, we enable the encoding of genuinely substructural logics in which some combination of ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2024
290 pages
ISBN:9798400704888
DOI:10.1145/3636501
- General Chairs:
- Amin Timany,
- Dmitriy Traytel,
- Program Chairs:
- Brigitte Pientka,
- Sandrine Blazy
Copyright © 2024 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 the author(s) 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
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 09 January 2024
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- Ministry of Science, Innovation and Universities, Spain
Conference
CPP '24
Sponsor:
CPP '24: 13th ACM SIGPLAN International Conference on Certified Programs and Proofs
January 15 - 16, 2024
London, UK
Acceptance Rates
Overall Acceptance Rate 18 of 26 submissions, 69%
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 148Total Downloads
- Downloads (Last 12 months)54
- Downloads (Last 6 weeks)5
Reflects downloads up to 03 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in