In the meantime, the VerifyThis competition
http://fm2012.verifythis.org/might be an interesting venue to trial a
HOL-family team. Anyone interested?
On Wed, Jun 6, 2012 at 1:59 PM, Ramana Kumar <[email protected]> wrote:
> On Wed, Jun 6, 2012 at 1:51 PM, Rob Arthan <[email protected]> wrote:
>
>> 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.
>>
>
> Although the problems were formulated in terms of imperative programs, in
> the latest competition solutions for functional versions of the same
> algorithms were also allowed. I think this will continue to be true in
> later competitions.
>
>
>>
>> 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.
>>
>
> Cool - I like the idea of a "HOL family" team. I don't see any reason why
> it would be unfair; "HOL family" is a reasonably coherent concept. In the
> last competition, teams of up to 4 people were allowed with very few
> restrictions. In particular, individuals can belong to more than one team,
> more than one piece of software can be used by a team, and the software can
> be modified during the competition.
>
>
>>
>> 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
