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 Σ d26ae6bb9a331c05347cabb1f80a9ae5baf7c817a6eab28c6c7fdeb8968bd68e
utils.v Π, Δ d03105891b2a87b0a4376f9caa52a36e3fc90463da60500c5dfe31132bc2c5e8
itv_topology.v Σ f3830a90b45cfe3a450fa60201ab42b0e0012074db22398159baf2ad4151a255
impl_data.v Σ, Π, Δ 37aaa08707b1cf1fa65eab6878bba72a1c661f90cddfc9600be358934ede19b6
impl_splitters.v Σ, Π, Δ 4217128b088f7d25c321e91012888f2c80d377a7d9136b5b17fdb035b1d13ba3
impl_FOs.v Σ, Π, Δ 2b699c14005cccfb7b73c3c9081e687aeae3faa032cf18db4a07d5fb75bb8964
impl_splittersR.v Σ, Π, Δ 14fb080206dcb25f9d80d77faf9f0553c87b55ffd6759cf421d3fdd19d67f5c5
impl_dataR.v Σ, Π, Δ c74cec2e5cefdf2cc6c326df68d6ec26a7c40ed38857b7731358d3202d798354
impl_FOsR.v Σ, Π, Δ ab6da144a9cb30626c1ce04406e0b9ca36d446ddfdce6a0b810f91c8987eafd7
impl_rules.v Σ, Π, Δ e9f98c1d261e1f7aeea4c3d809010aa1329206ecdb55cf09338737b4a30ca8eb
impl_rulesR.v Σ, Π, Δ ef8c043c82c37ec98f6444ca493525ef3f472e524b3b5ebd129289071c94f6e3
extract.v Π 2928b15b714b50c7030c2965eafa612b9744e16324679997abf78593c65c2854
verified_extraction_command.v Π 88ae3cb6d0b84b9672e1cf383b7165ed2ac9b8a394d1bd0514395222a6be168b
wfrec_extract.v Π f58c6dcfc1a27fbbaac0946103b93c98b5288f30e3859dbade90eb75a8c6d477
extract_correspondence.v Σ, Δ 9d628a6822d3b8f193e1a30f0ff64994ec4e345d20b0cd482c912a04a351f35c
splitters_ver.mlf Λ 78483b7da51ef74406330a71c7089dbdda5b8ecabda49e81b5079e77a4575952
splitters_ver.mli Λ ef511985194fe629429777e3759acf7711427e7e3f65990f5e713ff071a3ae97
(*) 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 fcd91e4d5f5eed443143ef0ec3272ecc72be446ae605be0744ff190d07263705
main.ml Code for command-line interface, written by FV 1adc2e66bac8c82d5d07c0f1c03e5b269145de9b352554842aa9c3a9095ea7df
hours_service_theory.pdf Document describing the mathematical formalization (Θ) 24660617d6fba500213f57dcb583c3aabeb57103058a1c115ae91c9788ff3740
fvhsd-tech-spech.pdf Documentation of the input/output and command-line interface e9c982b87232a92ca5153c15093e7539881d1714b8b1b39ec0eecadf8ddce835