2025/12/14 by Manuel Bentele, Bentele, Manuel, Andreas Podelski +5
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Software Engineering (cs.SE) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.2512.12788
openalex publication_date 2025/12/14 · openalex created_date 2025/12/17 · openalex updated_date 2026/07/28
Temporal HAL-API Dependencies (THADs) can be useful to capture an interesting class of correctness properties in embedded software development. They demand a moderate effort for specification (which can be done via program annotations) and verification (which can be done automatically via software model checking). In this sense, they have the potential to form an interesting sweet spot between generic properties (that demand virtually no specification effort, and that are typically addressed by static analysis) and application-specific properties as addressed by full-fledged formal methods. Thus, they may form a gateway to wider and more economic use of formal methods in industrial embedded software development.