FV Hours of Service of Drivers-561-395

Case

File

Presentation date

Certification approved date

2023-12 FV HSD-561-395

2026-01-27

2026-02-19

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_rules.v Σ, Π, Δ e9f98c1d261e1f7aeea4c3d809010aa1329206ecdb55cf09338737b4a30ca8eb
impl_dataR.v Σ, Π, Δ c74cec2e5cefdf2cc6c326df68d6ec26a7c40ed38857b7731358d3202d798354
impl_splittersR.v Σ, Π, Δ 14fb080206dcb25f9d80d77faf9f0553c87b55ffd6759cf421d3fdd19d67f5c5
impl_FOsR.v Σ, Π, Δ ab6da144a9cb30626c1ce04406e0b9ca36d446ddfdce6a0b810f91c8987eafd7
impl_rulesR.v Σ, Π, Δ ef8c043c82c37ec98f6444ca493525ef3f472e524b3b5ebd129289071c94f6e3
extract.v Π 5b42a6c313bc4362463921a5141de045532c082e66145ef1137f23a593a8469b
verified_extraction_command.v Π 916aed8756dad61f79cf114a541b8e1117baa3ef073364be760f8831608164fb
wfrec_extract.v Π f58c6dcfc1a27fbbaac0946103b93c98b5288f30e3859dbade90eb75a8c6d477
extract_correspondence.v Σ, Δ 9d628a6822d3b8f193e1a30f0ff64994ec4e345d20b0cd482c912a04a351f35c
splitters_ver.mlf Λ 5a7b507f43fcc93adb75b990d8df5d95ffd3d0a0835297eb2bc5b0379636f3a8
splitters_ver.mli Λ 088aa1ae6ef4f4f3c1f7dd047c3cf42e21431488b244106ccba47add82aea894
(*) Semi-verified until extraction verification is reached, see details on extraction.

Non Formally Verified Parts

File name Components Checksum
FV-HSD-561-395.fv Φ 28582e214a4345ebc8e9922613e0317a6b7fa9d3c8d3569986adae4c15f9dd9a
FV-HSD-561-395Latex1.pdf Φ abf310579b7c4e66b0c9b84195e6e5ecddc4fe2177da40b2ad3df956ed155481

Other presented parts

File name Description Checksum
splitters.exe Compiled command-line interface for Windows 9c49b0658365a9264ce60fb89a55de74aaaeb6b5977c4aa187c2219a0e0494ad
main.ml Code for command-line interface, written by FV eb1ab77d61baa156034dde203701f17cae414ed742063847a82cde3df89a5603
hours_service_theory.pdf Document describing the mathematical formalization (Θ) e51c923ca0865d0648450235b81a316283f00b0bc9bfd2446a8ffa80b320fcd6
fvhsd-tech-spec.pdf Documentation of the input/output and command-line interface e36229dc707118a82ea90df4135efb319f371ae414255a7adb1952741ed28654
FV-HSD-561-395Latex2.pdf Documentation for the OCaml extracted code e386e1024c040e243d2c2d486d3ef96b3708a6f7d1726fe392801d9a93b29de8