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 | Σ | d617b935ade84f3b8f93c55b75be6165abf84c7da89d9db74efa2aff2f65c029 | ||
| doe_of_yoeK.v | Π, Δ | 5629cfdc189972b5d170206f35ce54d6741f47cfa7a376fe9b8af68fa73515bc | ||
| Hinnant.v | Σ, Π, Δ | dbdf4e38dcb9c546c521b283ab9470ed5c36a0a6804c106f8c60a7c6aa3db69d | ||
| HinnantR.v | Σ, Π, Δ | 8ff18d89a50e679c312fe73b6082b490c439ca12bccd64a7f10827c89e14dd59 | ||
| formalTime.v | Σ, Π, Δ | 817988af8ac2e18f8c22d4c7fa861c5a71c51458ec7b142f5ce2eca34df01718 | ||
| formalTimeR.v | Σ, Π, Δ | 5647a597033523f4c9aae9fc813a259926897a445426eabd7062fa186e764e1c | ||
| fvtm_extraction.v | Π | 5097ee2a350dfd551c603540bee4ce7b749b8c3e88aa78337b43b0e38a09ec15 | ||
| verified_extraction_command.v | Π | 375758c660eceb319bc5f546a8045caaf98b15256bc2f4e29d33238dd3364e9c | ||
| fvtm_unix_extraction.v | Π | cf1558af108232a77b0bf4ca1b4ab7ecf0ecdcb759f782ce5b7ff9e53573abca | ||
| fvtm_bipm_extraction.v | Π | f6d7ec4bebe2b7bd1b8755b884a28e70a2354eb00e11daa6c711bdac6d3184e3 | ||
| fvtm_unix_correct.v | Σ, Δ | 9d8744562da9d480ccac424e124ed428acb3bd28ba406a4b7d8ceb864f179eb8 | ||
| fvtm_bipm_correct.v | Σ, Δ | 40a77c5a5e7b599aa6e44d365070b09a4ca7605d43a4ecef1e78184dea3ebc08 | ||
| fvtm_extraction_correct.v | Σ, Δ | f9b52f786837c3a8c6f3daf3a48bd2daaff822e88921d93af637aba955473f7f | ||
| FVTM.mli | Λ | 7aeb8b0ec6ef9a2261dafd9a84d0ddb15efb953f5474e8216224deb194d46fb3 | ||
| FVTM.mlf | Λ | d75904a6a569c42a3dc2ed902f249fb24119a742293485cadd749727c28e5f7c | ||
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 | 84d02d833d76616fa12cc2849739dce9e6ff9df9b8fc7b9dc4a7462838a549d7 | ||
| timemanager.exe (Linux) | Compiled command-line interface for Linux | e1b0dae8598baf154c2cb76384cb95aa55cd072195e861240d8d5341ee56d06d | ||
| timemanager.exe (Windows) | Compiled command-line interface for Windows | 379285d3b97a9a19f8af058a95b09855ad9a7585a11808754d18cc1e93a4398b | ||
| 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 | ||