Experiments

We have tested Kindspec on an Intel Core2 Quad CPU Q9300(2.50GHz) computer with 6 Gigabytes of RAM running K v3.4 on Maude v2.6, for inference tasks.

The following table summarizes our experimental results for benchmark programs that contain both cyclic and acyclic data structures.

The Program column includes a link to the source code of each program example.
The LOC column shows the program size (in lines of code).
The Function column indicates the name of the target function.
The #Observers column is the number of observer program functions.
The #Paths column shows the number of root-to-leaf symbolic paths in the deployed trees.
The #Extracted Axioms column reflects how many different axioms are retrieved from the final states of the paths.
The #Candidate axioms column indicates the number of overly general axioms.
the Final contact contract column indicates the final number of correct axioms that are distilled as a result of the whole process. It might happen that this number is smaller than #Extracted Axioms due to the reduction given by generalized candidate axioms subsuming more specific axioms.
the Output column contains the link to the text version of the output provided by the tool.

Program	LOC	Function	#Observers	#Paths explored	#Extracted axioms	#Candidate axioms	Final contract	Output
cyclic_lists.c	95	collapseC	3	22	8	2	4	Contract
insert.c	120	insert	5	17	10	3	5	Contract
insert.c	90	insert	5	16	9	3	4	Contract
deallocate.c	59	deallocate	2	5	5	1	2	Contract
reverse.c	70	reverse	4	7	6	1	3	Contract
delete_circular.c	69	delCircular	3	13	7	1	4	Contract
append.c	60	append	3	32	32	10	4	Contract

All benchmark examples are available for download here.