[bitc-dev] Verified Software: Theories, Tools, Experiments

[Guillaume FORTAINE]

Hello,

Here is an interesting link, showing us how hard is the "challenge" :-) !

http://wiki.se.inf.ethz.ch/vstte/index.php/Verified_Software:_Frequently_Asked_Questions

"Q27: We have had extraordinary improvements in SAT solving. What will 
be the role of decision procedures in this project? Does the project 
rely on inventions of new decision procedures? Are fast decision 
procedures key to the success of this project?
A: Fast decision procedures (or rather, constraint solvers) will play an 
essential role in the project. They will provide the reasoning engines 
for all the other kinds of verification technology, including heuristic 
proof search, resolution, and model checking. New and faster decision 
procedures will be very welcome, and they must also work well together 
with each other and with the tools which exploit them.
But there are many other technologies whose development is essential to 
the project, and all of them deserve the title of ‘key’."

Surely, you already know these tools, but a refresh isn't always bad :-) !:

-A generic constraint development environment :

http://www.gecode.org/

-The Coq tool is a formal proof management system :

http://coq.inria.fr/

-COmputational INfrastructure for Operations Research :

http://www.coin-or.org/


Other " Challenges " ;-) ! :

http://www.acadeuro.org/downloads2/Informatics_programme.pdf

An interesting page :

http://www2.imm.dtu.dk/~db/

Best Regards,

Guillaume FORTAINE