Using Timbuk to verify first-order and 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 (for compleness guarantee of equation generation) and this one (for handling of higher-order features). 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
First order functions
delete.txt	not (member A (delete A A_and_B_list))	P	0.01s	0.01s	trace	`comp.res`	Yes
delete2.txt	(member B (delete A A_and_B_list))	P	0.01s	0.01s	trace	`comp.res`	Yes
deleteBasic.txt	(delete A A_and_B_list) removes all occurences of A	P	0.01s	0.01s	trace	`comp.res`	Yes
reverseFirstOrder.txt	reverse [A,...A,B,...,B] does not produce lists with a A before a B	P	0.01s	0.03s	trace	`comp.res`	Yes
reverseFirstOrder2.txt	invsorted (reverse [A,...A,B,...,B])	P	0.02s	0.13s	trace	`comp.res`	Yes
incTree.txt	not (member 0 (increment nat_tree))	P	0.08s	1.05s	trace	`comp.res`	Yes
replaceTree.txt	not (member A (replace A C A_and_B_tree))	P	0.44s	6.13s	trace	`comp.res`	Yes
orderedTree.txt	ordered ordered_A_and_B_tree	P	0.16s	6.73s	trace	`comp.res`	Yes
insertTree.txt	ordered (insert A_and_B_list emptyTree)	-	Timeout	Timeout	-	-	-
orderedTreeTraversal.txt	sorted (infix-traversal ordered_A_and_B_tree)	P	0.13s	1.71s	trace	`comp.res`	Yes
orderTreeTraversalBug.txt	sorted (prefix-traversal ordered_A_and_B_tree)	C	0.2s	-	trace	-	-
split.txt	not(member B (fst (split [A,B,A,B,...]))) and not(member A (snd (split [A,B,A,B,...])))	P	404s	186s	trace	comp.res	Yes
Higher-order functions, using this encoding
mapPlus.txt	no 0 in (map (plus 1) nat_list)	P	0.02s	0.08s	trace	`comp.res`	Yes
filterEven.txt	not (exists even (filter odd nat_list))	P	0.12s	1.16s	trace	`comp.res`	Yes
filterEvenBug.txt	not (exists odd (filter odd nat_list))	C	0.09s	-	trace	-	-
insertionSort.txt	(sorted leq (sort leq A_and_B_list))	P	0.04s	0.11s	trace	`comp.res`	Yes
insertionSortBug.txt	(sorted geq (sort leq A_and_B_list))	C	0.59s	-	trace	-	-
filterNz.txt	(forAll nz (filter nz nat_list))	P	0.01s	0.11s	trace	`comp.res`	Yes
mapTree.txt	no 0 in (map (plus 1) nat_tree)	P	0.03s	16.15s	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.04s	0.47s	trace	`comp.res`	Yes
mapSquare.txt	(filter (eq 2) (map square nat_list)) is empty	P	0.31s	4.25s	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	0.05s	0.29s	trace	`comp.res`	Yes
foldLeftPlus.txt	even (foldLeft plus 0 even_nat_list)	P	0.01s	0.21s	trace	`comp.res`	Yes