4 papers
Checking the HAL Interface Specification Continuously, Right from the Start
Manuel Bentele, Onur Altinordu, Jan Körner +2
The correct use of a Hardware Abstraction Layer (HAL) interface in embedded applications is crucial to prevent malfunctions, crashes, or even hardware damage. Software model checki…
Relevant HAL Interface Requirements for Embedded Systems
Manuel Bentele, Andreas Podelski, Axel Sikora +1
Embedded applications often use a Hardware Abstraction Layer (HAL) to access hardware. Improper use of the HAL can lead to incorrect hardware operations, resulting in system failur…
Temporal HAL-API Dependencies as a Gateway to Formal Embedded Software Development
Manuel Bentele, Andreas Podelski, Axel Sikora +1
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 sp…
Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Extended Version)
Julian Erhard, Manuel Bentele, Matthias Heizmann +7
Static analyzers are typically complex tools and thus prone to contain bugs themselves. To increase the trust in the verdict of such tools, witnesses encode key reasoning steps und…