Case
File
Presentation date
Certification approved date
2022-01 - FV Time Manager
2022-01-12
2025-08-04
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 | ||
| verified_extraction_command.v | Π | 37c1ad7532e97cd0186c2964104904993c555e4a07eca17305f991ed852dd379 | ||
| fvtm_extraction_correct.v | Σ, Δ | 0d35048ab3754aac01ad5323f6a9f7c630482550e82087182eb4900daa7810d8 | ||
| FVTM.mli | Λ | 9b31c5284c22b157e1bf0bf2cf9f1f8b1f434975809790f236fb9e1504f1d867 | ||
| FVTM.mlf | Λ | 09ebbadcc90ec9ec6f8d6a45f1f4c67892c3a1332b9381df2c5d727755b17850 | ||
Non Formally Verified Parts
| File name | Components | Checksum | ||
|---|---|---|---|---|
| FV-Time.fv | Φ | b805fad9e0511d3739edeb0a1fe7794bbcd094205528c0616be9b0d8a4eafe1f | ||
| FV-TimeLatex1.pdf | Φ | 0451846b374939a0949fcb8f05c3bc15276a84bb46cbbc7ae2c07175af6d23c9 | ||
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 | ||
| FV-TimeLatex2.pdf | Documentation of the OCaml extracted code | d5260c44810beaede27ac9c4a53343784d571b0d64f1660e6143ea9bbeefa406 | ||
| DateTime Specifications.v.4.pdf | Document describing the original idea (Θ) | 3d23e410790b2055a08130bd70ddc58366bc0039400d4c26654d7693493b4902 | ||