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 Σ 4b0b9969e858370d7cd13515ee0df377770b5c91989e0c1afab85c69babe06fc
utils.v Π, Δ 4b0b9969e858370d7cd13515ee0df377770b5c91989e0c1afab85c69babe06fc
itv_topology.v Σ f87cd00bf459dae4598ca5be26ea49e5964d20796b5670cef0b9fa4f8cdfd128
impl_data.v Σ, Π, Δ 2d5225da9c5036b0b444cb9fcce1e0d6dbb9f471a615106a13c3d9bb2b98a8be
impl_splitters.v Σ, Π, Δ 21cdd001624b987a83f5eb31c3f8b5d62cb26ae8ad3a87695821e7fe008abad6
impl_FOs.v Σ, Π, Δ d1d98d8151177dbca22f3534ccfe7db89261a54fde302915fc71f0e66964270f
impl_splittersR.v Σ, Π, Δ 9ca3148fa193c8373f5b5e646590196f52230f14a4ae4832f8b9ab260a532d89
impl_dataR.v Σ, Π, Δ b7c58877f733667939d20683dca0078be90f54372ed05eab606ca58bcc964273
impl_FOsR.v Σ, Π, Δ 44b38daf997fd5fa186cc0cdefe8c7caa565c697dc3b4ba855b593f841f57f23
impl_rules.v Σ, Π, Δ 800d06a23225b84f522f203253d4a62b0d7a3859fa72e2b2d1f6291c766e069b
impl_rulesR.v Σ, Π, Δ 13f323c13bd8e2c8c4afb443a62b684e70f9aeed9be8be8f954248911bb8a758
extract.v Π fc3cc47708f2682ac4d89093de61f448b141494de13500c9b90394b113247fd8
extract_correspondence.v Σ, Δ be060b35f714d615891ff25d2f78fe0f426e1d9c6a607577e1e860722521e078
splitter_ext.ml* Λ a96c64a99bdec17818e22fd175ba5ba3e4502e27e0bb3b713d6d33758d236144
splitter_ext.mli* Λ 95215f60e5a65f5977336cc972eba80bc11e2d77bf4212591951d1926646be22
(*) 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 6db526be0527646d2785cd02e600aca98ce8aa7289a0190cc20eb250a9a05a38
main.ml Code for command-line interface, written by FV 41a510d1f7632421adbc139c448cf80fcad4849d1c1cadc109d31245577868d3
Formulation of Hours of Service of Drivers-561-395.pdf Document describing the mathematical framework 81a2c99a1e9a51553216e2b25238f1cc6095577c8c932689fe122dba7c0d4fb1
fvhsd-tech-spech.pdf Documentation of the input/output and command-line interface 3e36dfbb742b04c7f36152ba881d0b353bca21e00c6fc7a40275345517f4ec4e