{"ID":2846618,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2511.01417","arxiv_id":"2511.01417","title":"VeriODD: From YAML to SMT-LIB -- Automating Verification of Operational Design Domains","abstract":"Operational Design Domains (ODDs) define the conditions under which an Automated Driving System (ADS) is allowed to operate, while Current Operational Domains (CODs) capture the actual runtime situation. Ensuring that a COD instance lies within the ODD is a crucial step in safety assurance. Today, ODD and COD specifications are frequently expressed in YAML to remain accessible for stakeholders, but such descriptions are not directly suitable for solver-based verification. Manual translation into formal languages such as SMT-LIB is slow and error-prone. We present VeriODD, a tool that automates this translation. VeriODD uses ANTLR-based compiler technology to transform YAML-based ODD/COD specifications into both human-readable propositional logic, for lightweight review on a simple basis, and solver-ready SMT-LIB. The tool integrates with SMT solvers such as Z3 to provide automated consistency checks of ODD specifications and verification of COD conformance. A graphical user interface supports editing specifications, inspecting generated formulas, and performing verification with a single click. VeriODD thereby closes the gap between stakeholder-friendly ODD/COD notations and formal verification, enabling scalable and automated assurance of operational boundaries in autonomous driving. Video demonstration: https://youtu.be/odRacNoL_Pk Tool available at: https://github.com/BasselRafie/VeriODD","short_abstract":"Operational Design Domains (ODDs) define the conditions under which an Automated Driving System (ADS) is allowed to operate, while Current Operational Domains (CODs) capture the actual runtime situation. Ensuring that a COD instance lies within the ODD is a crucial step in safety assurance. Today, ODD and COD specifica...","url_abs":"https://arxiv.org/abs/2511.01417","url_pdf":"https://arxiv.org/pdf/2511.01417v1","authors":"[\"Bassel Rafie\",\"Christian Schindler\",\"Andreas Rausch\"]","published":"2025-11-03T10:11:29Z","proceeding":"cs.SE","tasks":"[\"cs.SE\"]","methods":"[]","has_code":false,"code_links":[{"ID":607446,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_id":2846618,"paper_url":"https://arxiv.org/abs/2511.01417","paper_title":"VeriODD: From YAML to SMT-LIB -- Automating Verification of Operational Design Domains","repo_url":"https://github.com/BasselRafie/VeriODD","is_official":false,"mentioned_in_paper":false,"mentioned_in_github":true,"github_stars":0}]}