RETOS

IP: Joost J. Joosten.

Funding: Ministry of Science and Universities, Retos Colaboración RTC-2017-6740-7 Software de fallo cero, grant of 825.704€, rentless loan of 284.672€; Co-financed through the ERDF scheme (European Regional Development Fund of the European Commission); Jan 2019 – May 2022.

The project is an effort to develop formally verified legal software for the application of the EU Regulation 561/2006 to the road transport industry. Current software is not subject to high standards of verification and may contain both detectable and undetectable "bugs", leading to contestable and uncontestable fines, some of which may be unfair and not legally warranted.

To this aim, the project is invested in research into desirable logical and metamathematical properties of a temporal and deontic ontology in order to ensure its computational implementability.

Moreover, the innovative approach tests and develops the capacity the Coq proof assistants, a tool that checks the correctness of mathematical proofs, for programming high-grade software for industry. The resulting code is delivered together with a proof that it meets its formal specification, excluding the possibility of both "bugs" as well as "bugless misinterpretations".