Verification of Tree-Processing Programs via Higher-Order Model Checking
------------------------------------------------------------------------------
append
append (with a wrong spec.)
reverse using append
reverse using append (with a wrong spec.)
insertion sort
insertion sort (with a wrong spec.)
merge sort
repeated homomorphism and reverse
Split from CDuce sample programs
Split (with a wrong annotation)
Bib2HTML from CDuce sample programs
XMark query 1
XMark query 2
Gapid-HTML from [Tozawa 2006]
JWIG-guess
JWIG-guess (with a wrong annotation)
JWIG-cal
JWIG-cal (with a wrong annotation)
k-normalization from MinCaml
------------------------------------------------------------------------------
reverse using an accumulator
reverse using an accumulator (with a wrong spec.)
reverse-append using an accumulator
XHTML transformation (remove "a" nodes and move the subtrees to the parent node)
repeated homomorphism