Using Timbuk to verify higher-order functional programs

Here is a collection of examples that have been automatically checked using the Timbuk library. The theoretical principles can be found in this report. Those experiments can be replayed by downloading and compiling Timbuk's last version (this is not yet available on the online version). This archive contains all the examples presented on this page in the funExperiments folder. The certification of results can also be replayed using the checker extracted from the Coq theory. On all the examples of this page the checker takes only a few milliseconds to certify the restult. Experiments were performed on a MacBook Pro 3.1 Ghz.

Timbuk Specification	Description	(P)roof/(C)ounterexample	Completion Time	Equation Generation Time	Timbuk Output	`comp.res`	Certified by Coq checker
filterEven.txt	not (exists even (filter odd nat_list))	P	0.06s	27.89s	trace	`comp.res`	Yes
filterEvenBug.txt	not (exists odd (filter odd nat_list))	C	1.24s	-	trace	-	-
insertionSort.txt	(sorted leq (sort leq A_and_B_list))	P	0.54s	1.11s	trace	`comp.res`	Yes
insertionSortBug.txt	(sorted geq (sort leq A_and_B_list))	C	31.44s	-	trace	-	-
filterNz.txt	(forAll nz (filter nz nat_list))	P	0.02s	0.97s	trace	`comp.res`	Yes
mapTree.txt	no 0 in (map (plus 1) nat_tree)	P	0.04s	270.37s	trace	`comp.res`	Yes
mapTree2.txt	not(member 0 (map (plus 1) nat_tree)	-	Timeout	Timeout	-	-	-
mapTree2NoGen.txt	not(member 0 (map (plus 1) nat_tree)	P	0.08s	No Generation	trace	`comp.res`	Yes
reverse.txt	(sorted geq (reverse ordered_A_B_list))	P	0.06s	20.10s	trace	`comp.res`	Yes
mapSquare.txt	(filter (eq 2) (map square nat_list)) is empty	P	0.33s	24.92s	trace	`comp.res`	Yes
foldRightMult.txt	(foldRight mult nonzero_nat_list 1) is not 0	P	0.01s	0.01s	trace	`comp.res`	Yes
foldRightMult2.txt	(foldRight mult nonzero_nat_list 3) is not 2	P	1.51s	331.51s	trace	`comp.res`	Yes
foldLeftPlus.txt	even (foldLeft plus 0 even_nat_list)	P	1.44s	223.64s	trace	`comp.res`	Yes