1

Precise Widening Operators for Proving Termination by Abstract Interpretation

Büchi, Lindenbaum, Tarski: A Program Analysis Appetizer

Synthesizing Ranking Functions from Bits and Pieces

Abstract Interpretation as Automated Deduction

Conflict-Driven Conditional Termination

FuncTion: An Abstract Domain Functor for Termination (Competition Contribution)

Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation

A Decision Tree Abstract Domain for Proving Conditional Termination

An Abstract Domain to Infer Ordinal-Valued Ranking Functions

The Abstract Domain of Segmented Ranking Functions