FV Hours of Service of Drivers-561-395

Case

File

Presentation date

Certification approved date

2023-12 FV HSD-561-395

2023-12-20

pending

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 Σ b7bab91f08572774055eb5a9fb81097daa1525cfee39031409facf841b5d35d1
utils.v Π, Δ a209af21b8b20e239083fcea80ef827bd930462a47e1d81e0b81cc84739b27cc
itv_topology.v Σ 760f60fb632c8e4baa3da4797f55e20e17c4b2c62372619340cc9c9c6eda9b42
impl_data.v Σ, Π, Δ 2e16bee24aa359318a7c8bfb217bd8d13f6432208e38aa1a30813c09cfe1205b
impl_splitters.v Σ, Π, Δ 537be67c5b8a4b1edfba9586d9b35bb50d2f804f638a2d85722803e769b4d451
impl_FOs.v Σ, Π, Δ e64a6ff712f154029e68eea9c0946ae8cb17dba828b406c725d2527dee9ea9d0
impl_splittersR.v Σ, Π, Δ 18b06ba98b337bd15d78ccdbcead1179f39c69f9f57d52394e562e3869de45bf
impl_dataR.v Σ, Π, Δ 79e9cd6ecb873c652d233e07d73365a144c71fed7f6edd40cbbd5917bdf180fd
impl_FosR.v Σ, Π, Δ 21fc08daf716068b190dfd00462aec280614b03374d2f0e13730bc6e6825adef
impl_rules.v Σ, Π, Δ d669ad90e7a3ac0b4044bc991cdfae1b6940c0588612202ce6121eaca6ed5aa6
impl_rulesR.v Σ, Π, Δ 21768c07b495e724a4f6d1d81d42fa2d610bab0adf90aadaec99bc60ce5f5d9f
extract.v Π ccd63999863a624dabfe072bc354bc1b870f6792e3fc5517fb0a62bac41f4c57
extract_correspondence.v Σ, Δ 6cb7c56e7901c1557d2141525aaee58461e45ca48114cb50b13dabad978ff88e
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-PCWH-phi.pdf Φ (in construction)

Other presented parts

File name Description Checksum
uint63.mli Interface for OCaml machine integers, provided by Coq 83d67014936c9a2e6007f2a16e7a40446de7bd505fad7a19b60f98ae6f61f8c1
uint63.ml Code for OCaml machine integers, provided by Coq 46e6a6412db8dab76aea9b0fab125ea2251f8628f16291f30ed2042f31cd5d16
splitters.exe Compiled command-line interface for Windows 8d660637c07836763e0f88d5794878999529beb7a7b589d1e60213741dc93d26
main.ml Code for command-line interface, written by FV 9a48c6992b74ecbc839a1b9f5ba081d02c4daabd69ed20269bf45ba0fa165682
Formulation of Hours of Service of Drivers-561-395.pdf Document describing the mathematical framework ba1fbd83c35e067a10e68add6f395651521d81a9b11f18366236d9c3608cd871
fvhsd-tech-spech.pdf Documentation of the input/output and command-line interface e9c982b87232a92ca5153c15093e7539881d1714b8b1b39ec0eecadf8ddce835