Some programs that need polynomial invariants in order to be verified  


cohendiv
divbin
hard
mannadiv
wensley

sqrt
dijkstra
z3sqrt
freire1
freire2

euclidex1
euclidex2
euclidex3
 
lcm1
lcm2

prodbin
prod4br
 
fermat1
fermat2
knuth

cohencu 
readers_writers
petter

illinois
mesi
moesi
berkeley
firefly