An example of program verification: the N-queens problem
This page presents the formal verification with the Why and
Caduceus tools of the following C program:
t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b+d)*2,(
c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q),0,0));}
This program was written by Marcel van Kervinc and found on
this page.
