see also the index (by topic, by tool, by reference, by year)
http://caduceus.lri.fr/
A deductive verification tool for C programs.