Case
File
Presentation date
Certification approved date
2022-01 - FV Time Manager
2022-01-12
2022-04-02
General details
Presented by
Address
Country
Tax id
Represented by
Position
Public Name for public certified software
Formal Vindications S.L
Carrer del Bruc, 21, 2º-4ª, Barcelona
Spain
B66843327
Guillermo Errezil
Main Manager
FV Time Manager
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 | ||
Non Formally Verified Parts
| File name | Components | Checksum | ||
|---|---|---|---|---|
| fv-time-phi.pdf | Φ | 4bceb001d5247b3cfb0b5b22bfcdf320a4b787c2d024b01c02aa91a9258560e8 | ||
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 Windows | c959332baaf78414d826ec5cbaddd3c0414b45acf12ffe281eaabe0fd0ac291d | ||
| fvtm-tech-spec.pdf | Documentation of the command-line interface | 497c30d8367bf1b85c4525b67f306e1cde993109588d143ae88e4a6692322e3a | ||
| fvtm-ocaml.pdf | Documentation of the OCaml extracted code | 650b5e92e4ea6e38f5b4efe17bd582a871c0c6e85fb10d683bd1fec009a0f0c6 | ||