Case
File
Presentation date
Certification approved date
2023-12 FV HSD-561-395
2023-12-20
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
Hours of Service of Drivers-561-395
Formally Verified Parts
File name | Components | Checksum | ||
---|---|---|---|---|
spec.v | Σ | bafd84e3b05ec21dc4b7c02d7a00254f5ae31037dd6e5aaacbe1a64baa82eabd | ||
utils.v | Π, Δ | a209af21b8b20e239083fcea80ef827bd930462a47e1d81e0b81cc84739b27cc | ||
itv_topology.v | Σ | 760f60fb632c8e4baa3da4797f55e20e17c4b2c62372619340cc9c9c6eda9b42 | ||
impl_data.v | Σ, Π, Δ | d1e692c22ee9f44f343fa1b5f2e462915a15be8217b6306959a1f884b15d4b2a | ||
impl_splitters.v | Σ, Π, Δ | 537be67c5b8a4b1edfba9586d9b35bb50d2f804f638a2d85722803e769b4d451 | ||
impl_FOs.v | Σ, Π, Δ | e64a6ff712f154029e68eea9c0946ae8cb17dba828b406c725d2527dee9ea9d0 | ||
impl_splittersR.v | Σ, Π, Δ | 18b06ba98b337bd15d78ccdbcead1179f39c69f9f57d52394e562e3869de45bf | ||
impl_dataR.v | Σ, Π, Δ | 42fad35fcee51a5a1be53e3a1c639842bc9a7d17cb9aaa5faa0f06140896a144 | ||
impl_FosR.v | Σ, Π, Δ | 21fc08daf716068b190dfd00462aec280614b03374d2f0e13730bc6e6825adef | ||
impl_rules.v | Σ, Π, Δ | d7c670482157ee6a4ea7becdd332da23c8b41592a663a13cdb54ab811189b915 | ||
impl_rulesR.v | Σ, Π, Δ | 21768c07b495e724a4f6d1d81d42fa2d610bab0adf90aadaec99bc60ce5f5d9f | ||
extract.v | Π | ccd63999863a624dabfe072bc354bc1b870f6792e3fc5517fb0a62bac41f4c57 | ||
verified_extraction_command.v | Π | 68ed75fd5fa4994d63775f598ad947f2de553045086d401848f4e9f53eb99691 | ||
wfrec_extract.v | Π | 705542d0b68a5da1cda041a24b9a6ea695eddbcf3ac42eadcc76e169e11cb9cb | ||
extract_correspondence.v | Σ, Δ | d45917fcd4a14bca6aab7a73720921661d4a85b53f262b5ae007336cd38464f3 | ||
splitters_ver.mlf | Λ | f37be0bca8667ba7f11ee7328c2f36e02a907cbbd6f26e66403d3ba3dd100e75 | ||
splitters_ver.mli | Λ | bab63da98edf12a117d5bae98f87c592a4870c05b4614b30580c63a0f45ac208 |
Non Formally Verified Parts
File name | Components | Checksum | ||
---|---|---|---|---|
FV-HSD-561-395.fv | Φ | c03801a2b8d3b937e1861a3c86907d143d5d60a6d1c443a31430e1aa4e941858 | ||
FV-HSD-561-395Latex1.pdf | Φ | ff932d804f26e8e24d016736dd7d59663fd822ea5f7afce83f9d98ffed2c95c1 |
Other presented parts
File name | Description | Checksum | ||
---|---|---|---|---|
FV-HSD-561-395Latex2.pdf | Documentation for the OCaml extracted code | 6d8d19a4eaddfabc1fca431218f6b2d3e515ed50aab41a2193f0f7a65542d508 | ||
splitters.exe | Compiled command-line interface for Windows | 8d660637c07836763e0f88d5794878999529beb7a7b589d1e60213741dc93d26 | ||
main.ml | Code for command-line interface, written by FV | 9a48c6992b74ecbc839a1b9f5ba081d02c4daabd69ed20269bf45ba0fa165682 | ||
hours_service_theory.pdf | Document describing the mathematical formalization (Θ) | 24660617d6fba500213f57dcb583c3aabeb57103058a1c115ae91c9788ff3740 | ||
fvhsd-tech-spech.pdf | Documentation of the input/output and command-line interface | e9c982b87232a92ca5153c15093e7539881d1714b8b1b39ec0eecadf8ddce835 |