Proving Autonomous Vehicle and Advanced Driver Assistance Systems Safety: Final Research Report

Fulton, Nathan; Ji, Ran; Platzer, Andre · 2016 · ROSA P / Technologies for Safe and Efficient Transportation. University Transportation Center

archive: archived pipeline: cataloged verified

Get this paper ↗ (full text — opens at the source; we link to it, we don't host it)

Summary

This research report addresses the critical challenge of verifying the safety and correctness of autonomous vehicles and advanced driver assistance systems, which are classified as cyber-physical systems (CPS). The authors argue that traditional validation methods, such as simulation, are insufficient because they cover only a minuscule fraction of the relevant state space. To provide undeniable mathematical evidence for safety claims, the project focuses on formal verification using logic. Specifically, it aims to improve tooling for CPS verification by developing a new theorem prover, KeYmaera X, and establishing a logical foundation for proof certificates through the Logic of Proofs for Differential Dynamic Logic (LPdL). The methodology centers on extending differential dynamic logic (dL), a logic used to specify and verify properties of hybrid systems that combine discrete computation with continuous dynamics. The authors developed KeYmaera X, a theorem prover based on a uniform substitution calculus for dL, featuring a minimal soundness-critical core of fewer than 2,000 lines of code. This design isolates axiomatic reasoning to prevent subtle errors while allowing for experimental features. The core contribution is LPdL, which augments dL with explicit proof terms. These terms serve as syntactic representations of logical deductions, providing first-class access to safety properties and their certificates. LPdL supports equivalence rewriting, uniform renaming, and uniform substitutions, enabling the composition, reuse, and parameterization of proofs. The primary findings include the presentation of a semantic model for LPdL that extends standard reachability relation semantics with a notion of evidence. The authors established the correctness of this logic by proving that all evidence pieces in LPdL correspond to valid deductions in dL. Furthermore, they demonstrated how these results facilitate the construction of a proof term checker for LPdL without extending the soundness-critical core of the theorem prover. This approach provides a clean separation between proof checking and proof search, addressing limitations in previous systems like KeYmaera. The report also highlights that LPdL supports the synthesis of deterministic controllers from non-deterministic models, bridging the gap between CPS models and software implementations. The significance of this work lies in providing a rigorous logical foundation for hybrid systems with explicit evidence, which is essential for certifying safety-critical autonomous technologies. By enabling the persistence and communication of safety certificates to stakeholders and authorities, LPdL offers a theoretically well-founded method for verifying dynamic safety claims. The development of KeYmaera X and LPdL advances the field by improving the scalability and trustworthiness of formal verification tools, allowing for the application of rigorous mathematical proofs to increasingly complex traffic domains and CPS architectures.

Key finding

The Logic of Proofs for Differential Dynamic Logic (LPdL) provides a formal foundation for generating and verifying safety certificates for autonomous vehicles by extending differential dynamic logic with explicit proof terms that correspond to valid logical deductions.

Methodology

theoretical

Provenance

The full processing record for this entry. Every stage of this paper's journey through the pipeline is logged — what ran, with which tool and model, how many attempts it took, and when it last completed. Discovered via bulk_ingest_rosap on 2026-05-23 (6 acquisition events logged).

Summary generated by qwen3.6-27b-prismaquant on 2026-06-10; verification: verified.

Topics

Ranked by relevance to this paper. Hover a topic for its definition.

• driverless ads