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 | Σ | 6beb4b7e9b716409c5960a112767eaba901f02dba7e7bdeb93d3928010550e40 | ||
| doe_of_yoeK.v | Π, Δ | 38a0c582169dc6fb46fd56f811c1f123b71764075e4c9b1765ea90b73b857bc3 | ||
| Hinnant.v | Σ, Π, Δ | 18a7a49030b241ab7085378a30f8db66a77a915ba3882172cdfade0b1c104569 | ||
| HinnantR.v | Σ, Π, Δ | 73406d5849f8b1a9ebeee5bd7dcdd24526949d5d5271b2768be1465dae60212c | ||
| formalTime.v | Σ, Π, Δ | b7b45b8eea48cd6aa104d4ec4316eb4055753dd4a5069b3b5c4d2273b47f62ac | ||
| formalTimeR.v | Σ, Π, Δ | 5493eec207d42b48c47f95c36798d380a04fa62adf04051f5169f7449ef4660b | ||
| fvtm_extraction.v | Π | de7c56a17cddf08f9f1e72d3e5a3c52f9d5b5140be60ef4e112330bef2ac6473 | ||
| fvtm_extraction_correct.v | Σ, Δ | 0d35048ab3754aac01ad5323f6a9f7c630482550e82087182eb4900daa7810d8 | ||
| FVTM.mli | Λ | 9b31c5284c22b157e1bf0bf2cf9f1f8b1f434975809790f236fb9e1504f1d867 | ||
| FVTM.mlf | Λ | 09ebbadcc90ec9ec6f8d6a45f1f4c67892c3a1332b9381df2c5d727755b17850 | ||
Non Formally Verified Parts
| File name | Components | Checksum | ||
|---|---|---|---|---|
| fv-time-phi.pdf | Φ | 4bceb001d5247b3cfb0b5b22bfcdf320a4b787c2d024b01c02aa91a9258560e8 | ||
Other presented parts
| File name | Description | Checksum | ||
|---|---|---|---|---|
| timemanager.ml | Code for command-line interface, written by FV | a2c9dd74a77f4a262a1d3dd9fca3f11b4ee033f4d94896125fe8d6352659b668 | ||
| timemanager.exe (Linux) | Compiled command-line interface for Linux | 21fa8f627253a3306f0765149c8666638575ad653af59f9f84c52cb9002bd5c5 | ||
| timemanager.exe (Windows) | Compiled command-line interface for Windows | a4712255a1625059085ef0d5d6172d96dc92b93a3e91ca3513ac9a66434bb47b | ||
| fvtm-tech-spec.pdf | Documentation of the command-line interface | 497c30d8367bf1b85c4525b67f306e1cde993109588d143ae88e4a6692322e3a | ||
| fvtm-ocaml.pdf | Documentation of the OCaml extracted code | 650b5e92e4ea6e38f5b4efe17bd582a871c0c6e85fb10d683bd1fec009a0f0c6 | ||