[bitc-dev] Verified Software: Theories, Tools, Experiments
guillaume.fortaine at wanadoo.fr
Sun Aug 6 20:08:42 EDT 2006
Here is an interesting link, showing us how hard is the "challenge" :-) !
"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 :
-The Coq tool is a formal proof management system :
-COmputational INfrastructure for Operations Research :
Other " Challenges " ;-) ! :
An interesting page :
More information about the bitc-dev