FV Time

1. Case

File

2022-01 - FV

Presentation date

2022-01-12

Certification approved date

2022-04-02

2. General details

Presented by

Formal Vindications S.L

Address

Carrer del Bruc, 21, 2º-4ª, Barcelona

Country

Spain

Tax id

B66843327

Represented by

Guillermo Errezil

Position

Main Manager

Public Name for public certified software

FV Time

3. Formally Verified Parts

File name Components Checksum
calendar.v Σ db59f16a185b8942c505c6c18148cac9c66df0f590b9b12b983f35dff54bc09a
doe_of_yoeK.v Π, Δ 38a0c582169dc6fb46fd56f811c1f123b71764075e4c9b1765ea90b73b857bc3
Hinnant.v Σ, Π, Δ 4f4b72abf2fea1478ffda3cd74bfae73551ba55abe8c1138ffdf4386ea5c26dd
HinnantR.v Σ, Π, Δ f05e7eeef485d841e7b6eb39030bc1299f974c698c835943f6972915f54a89d6
formalTime.v Σ, Π, Δ f32e2ca0247e41e4f6cb4f32149e2dd3003e3bfb35205d02d22ef129d8ed3b71
formalTimeR.v Σ, Π, Δ 867b9c48c0a953f2ee13a37e01511f56741833114580f9f57a23a5174f006044
fvtm_extraction.v Π 5a8e37db1566e66a160687021a40ff1e799120a5c2114f3f9adbcce479a0b170
fvtm_extraction_correct.v Σ, Δ 4db59d6b667d2a9e49310a3259c53b1efa5fb05aa96d419152c51fe78910fa4d
FVTM.mli* Λ 08764b54381351d5b14e36339a9853274ad2f7c0e7ee5ed7388e5dd1c74e99c5
FVTM.ml* Λ 16d4cac53bf9f976bfbffa029903b518f33197a18cbde6f2b13edd3be87deb89

(*) Semi-verified until extraction verification is reached, see details on extraction.

4. Non Formally Verified Parts

File name Components Checksum
fv-time-phi.pdf Φ 4bceb001d5247b3cfb0b5b22bfcdf320a4b787c2d024b01c02aa91a9258560e8

5. Other presented parts

File name Description Checksum
uint63.mli Interface for OCaml machine integers, provided by Coq 83d67014936c9a2e6007f2a16e7a40446de7bd505fad7a19b60f98ae6f61f8c1
uint63.ml Code for OCaml machine integers, provided by Coq 46e6a6412db8dab76aea9b0fab125ea2251f8628f16291f30ed2042f31cd5d16
timemanager.ml Code for command-line interface, written by FV 279b560e857acb15df4ede44f14d80680b18ef4949b44d6b037ae96aff413483
timemanager.exe (Linux) Compiled command-line interface for Linux af62ee71aaa53b83fb6ed2cfd66521c67e05d7ef688a18eecfd34fcc644dead1
timemanager.exe (Windows) Compiled command-line interface for Linux c959332baaf78414d826ec5cbaddd3c0414b45acf12ffe281eaabe0fd0ac291d
fvtm-tech-spec.pdf Documentation of the command-line interface 497c30d8367bf1b85c4525b67f306e1cde993109588d143ae88e4a6692322e3a
fvtm-ocaml.pdf Documentation of the OCaml extracted code 650b5e92e4ea6e38f5b4efe17bd582a871c0c6e85fb10d683bd1fec009a0f0c6