FV Hours of Service of Drivers-561-395

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
(*) Semi-verified until extraction verification is reached, see details on extraction.

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