Dear HOL users
Would anyone be interested in entering a team using HOL4 or HOL Light to
the "Verified Software: Theories, Tools and Experiments" competition next
year (2013)?
Information about the last competition is here:
https://sites.google.com/site/vstte2012/.
Winning teams used ACL2, KIV, Dafny, PVS, or VCC. I hear people made
submissions using Isabelle and Coq, but apparently they didn't do as well.
I don't know of anyone who tried using HOL4 or HOL Light.
Next year's competition is probably several months away. I think it's a
good opportunity to look at why HOL-based provers don't do so well (is it
because the questions are biased against our tools, or because our tools
suck, or because our community is too weak to put together a good team?)
and improve our tools if necessary.
Cheers,
Ramana
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
