Verification of relational properties on programs manipulating ADTs
We provide one experiment:
The results with convoluted tree automata (FSCD'23 paper)
.