Proof Development:

The archive of vernacular files (Coq v6.3.1)

Reference:

Pierre Letouzey and Laurent Théry, ``Formalizing Stålmarck's algorithm in Coq'', TPHOLs2000, LNCS 1869, August 2000.

Trying it on examples:

You can try our extracted program on small examples (running time < 1 minute). Click here

Benchs:

The extracted program is a 1000 line long Ocaml program. Here are some computation times on a PC 450MHz

Example	Time	Example	Time	Example	Time
u1	0m0.009s	u2	0m0.013s	rip06_be	0m1.606s
syn041_1	0m0.009s	syn323_1	0m0.011s	add1_be	0m0.767s
syn046_1	0m0.011s	syn029_1	0m0.013s	rip08_be	0m3.093s
set043_5	0m0.011s	syn052_1	0m0.011s	aim_50_1_6_no_1	0m1.784s
lcl230_2	0m0.011s	syn051_1	0m0.012s	counter_be	0m6.429s
syn040_1	0m0.018s	syn044_1	0m0.011s	x1dn_be	0m24.297s
lcl181_2	0m0.011s	syn032_1	0m0.014s	vg2_be	0m13.296s
syn045_1	0m0.014s	syn011_1	0m0.012s	misg_be	0m7.675s
syn318_1	0m0.012s	syn030_1	0m0.012s	sqn_be	0m5.892s
syn047_1	0m0.012s	transp_be	0m0.018s	dubois20	0m7.398s
syn061_1	0m0.015s	syn054_1	0m0.012s	aim_100_1_6_no_4	0m31.516s
syn008_1	0m0.012s	gra001_1	0m0.019s	aim_100_1_6_no_1	0m28.658s
syn028_1	0m0.012s	syn321_1	0m0.018s	z5xpl_be	0m34.522s
syn060_1	0m0.012s	rip02_be	0m0.031s	dubois21	0m8.873s
syn062_1	0m0.015s	puz014_1	0m0.020s	add2_be	0m17.249s
puz004_1	0m0.063s	ztwaalf1_be	0m1.136s	dubois22	0m10.914s
puz002_1	0m0.010s	ztwaalf2_be	0m0.365s	f51m_be	0m32.952s
syn053_1	0m0.025s	z4_be	0m0.223s	dubois23	0m11.180s
syn057_1	0m0.012s	puz030_2	0m0.183s	dubois24	0m13.819s
syn055_1	0m0.071s	puz030_1	0m0.060s	dubois25	0m15.807s
puz033_1	0m0.022s	syn071_1	0m0.047s	aim_100_2_0_no_2	0m51.297s
puz029_1	0m0.107s	aim_50_1_6_no_3	0m0.475s	aim_100_2_0_no_3	1m6.669s
puz009_1	0m0.017s	aim_50_1_6_no_4	0m0.124s	aim_100_2_0_no_4	0m58.412s
puz013_1	0m0.030s	aim_50_1_6_no_2	0m0.164s	dubois26	0m16.798s
syn058_1	0m0.014s	hostint1_be	0m0.353s	dubois27	0m20.876s
syn063_1	0m0.026s	dk27_be	0m0.544s	dubois28	0m22.193s
puz003_1	0m0.030s	aim_50_2_0_no_1	0m0.279s	dubois29	0m23.411s
syn009_1	0m0.034s	aim_50_2_0_no_2	0m0.264s	z9sym_be	1m16.915s
spoor4_neg	0m0.056s	aim_50_2_0_no_3	0m0.264s	dubois30	0m27.478s
spoor2_neg	0m0.069s	aim_50_2_0_no_4	0m0.254s	add3_be	10m48.552s
spoor3_neg	0m0.135s	mul03_be	0m0.155s	dubois50	1m59.788s
puz012_1	0m0.573s	mul_be	0m0.294s	aim_200_2_0_no_1	10m17.533s
heerhugo3_neg	1m2.303s	dk17_be	0m1.816s	aim_200_2_0_no_3	21m17.042s
ssa6288_047	172m47.100s	risc_be	0m1.428s	aim_200_2_0_no_4	12m17.398s
		msc006_1	0m0.094s	mlp4_be	297m33.754s
		aim_100_1_6_no_3	0m0.811s
		dc2_be	0m4.475s
		syn072_1	0m0.130s
		root_be	0m18.836s
		aim_100_2_0_no_1	0m0.991s
		prv001_1	0m0.133s
		aim_200_1_6_no_4	0m6.674s
		aim_200_1_6_no_2	0m6.912s
		rom2_be	1m1.556s
		ssa0432_003	0m14.483s
		table_be	4m57.163s
		jnh211	0m36.187s

Warning:

Stålmarck's method is patented and should not be used for commercial applications without the agreement of Prover Technology. For more information, check this.