The Coq mailing list

[Claude Marche <Claude.Marche AT inria.fr>]

Le 05/06/2012 03:21, Thomas Braibant a écrit :
> Hi coq-club,

Hi,

> Lately, I had the opportunity to attend a very interesting talk about
> Dafny [1], which highlighted the recent VSTTE competition (talk about
> the  results at [2]). From the results, it seem that 7 teams made a
> submission that was using Coq. Unfortunately, I cannot find any using
> a search engine. So, I am turning to the coq-club list, hoping that
> some of these people would agree to make their submissions public, and
> discuss them.

I'd like to mention that the solutions provided by Jean-Christophe and 
Andrei make a significant use of Coq, although not performed fully in 
Coq but with the Why3 system. They are available at URL 
http://proval.lri.fr/gallery/vscomp2012.en.html

Moreover, I believe that the various invariants introduced in the Why3 
source code can easily be reused to perform a proof in other proof 
environment.

> Now, on an higher level: looking at the variety of entries in the
> competition, and the set of problems, I think that the VSTTE
> competition is a good example of stuff that could foster some "cross
> community" interaction (say, "this is how people formalise this very
> same problem in Foo, and Bar"), and as such, the Coq community may
> gain something of having public and well-crafted solutions [3].

I'd like to take this opportunity to advertise the next VerifyThis 
competition that will take place at the next FM conference at the end of 
August. http://fm2012.verifythis.org/

Taking that this event will take place in Paris intra-muros, I guess 
that several Coq users may attend!

See also the next COMPARE workshop taking place during the IJCAR 
conference: http://compare2012.verifythis.org/ were various matters 
about "verification competitions" will be addressed.

Hope this helps,

- Claude


--
Claude Marché                          | tel: +33 1 72 92 59 69
INRIA Saclay - Île-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |