Tom Ridge and I formed two teams of one each using HOL4 and ProofPower-HOL
(respectively) in the first VSTTE competition which was a slightly smaller
scale affair at the previous VSTTE (it was a rather open-ended 2 hours during
the conference rather than 48 hours strictly timed several weeks before). Tom
and I both verified functional implementations written as recursive functions
in the HOL object language. Several of the questions in the second competition
were formulated in terms of imperative programs - so it was good to see that
that didn't stop ACL-2 coming joint first. I didn't participate in the second
competition because I didn't have anything like 2 days to spare.
Depending on my availability, I wouldn't mind joining a "HOL family" team, with
individuals using the HOL of their choice. But that might not be considered
fair.
Regards,
Rob.
On 6 Jun 2012, at 11:24, Ramana Kumar wrote:
> 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
------------------------------------------------------------------------------
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
