62 citations · 104 across the 15 of their papers we have counts for
8 papers · 1 filter
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 Prophecy for Proving Temporal Properties of Infinite-State Systems
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan +3
Various verification techniques for temporal properties transform temporal verification to safety verification. For infinite-state systems, these transformations are inherently imp…
Ultimate TreeAutomizer (CHC-COMP Tool Description)
Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke +2
We present Ultimate TreeAutomizer, a solver for satisfiability of sets of constrained Horn clauses. Constrained Horn clauses (CHC) are a fragment of first order logic with attracti…
Refining Trace Abstraction using Abstract Interpretation
Marius Greitschus, Daniel Dietsch, Andreas Podelski
The CEGAR loop in software model checking notoriously diverges when the abstraction refinement procedure does not derive a loop invariant. An abstraction refinement procedure based…
Proving Liveness of Parameterized Programs
Azadeh Farzan, Zachary Kincaid, Andreas Podelski
Correctness of multi-threaded programs typically requires that they satisfy liveness properties. For example, a program may require that no thread is starved of a shared resource,…
Termination Analysis by Learning Terminating Programs
Matthias Heizmann, Jochen Hoenicke, Andreas Podelski
We present a novel approach to termination analysis. In a first step, the analysis uses a program as a black-box which exhibits only a finite set of sample traces. Each sample trac…
Linear Ranking for Linear Lasso Programs
Matthias Heizmann, Jochen Hoenicke, Jan Leike +1
The general setting of this work is the constraint-based synthesis of termination arguments. We consider a restricted class of programs called lasso programs. The termination argum…