Re: [isabelle] The VSTTE'12 Modeling and Verification Competition



Hi,

we (Fabian Immler, Thomas Türk, Peter Lammich, and me) also attended the
competition, but lost due to an modelling error in Problem 2
(Combinators). We introduced the context only as a type and did not use
a predicate to restrict the left side of function application to values.

We not only used Isabelle/HOL, but Thomas used HOL4/HOL-Foot to model
problem 1 and problem 2.

-------------------------------------
Final score: 585 / 600

Rank: 7

Comments:
- Problem 2: definition of "red" does not impose the context C to have
  values on the lhs of applications. (-10 points)
- Problem 3: the definition of ring_buffer is somewhat difficult to read.
-------------------------------------

If you want to see our submission, you can find it here:

http://groups.google.com/group/vstte-2012-verification-competition/msg/c4073adfca97b904

Greetings,
  Johannes

Am Samstag, den 04.02.2012, 13:26 +0100 schrieb Burkhart Wolff:
> Dear all,
> 
> apparently I was the only one from the Isabelle community that 
> was present at the awards show of the VSTTE 2012 competition.
> I will therefore give a brief report and share some observations
> which might be relevant for teams that are interested to
> participate in future instances of this event.
> 
> 
> The VSTTE Modeling and Verification contest 
> (https://sites.google.com/site/vstte2012/compet/)
> is an  open competition for all sorts of modeling and verification 
> environments. To be solved in about 2 days  by fixed teams 
> up to 4 members, the problems  are from the domain
> of verification of sequential algorithms
> (see https://docs.google.com/viewer?a=v&pid=sites&srcid=ZGVmYXVsdGRvbWFpbnx2c3R0ZTIwMTJ8Z3g6OWE2MjQ3YzA5ZmRjOWQ4
> for the problem description sheet).
> The algorithms are so generic that they
> could be addressed by Isabelle/Simpl, but also
> in Isabelle/HOL directly. Termination proofs of nonstandard
> recursions were an important part of the problem solutions.
> 
> The submission to the competition ended 10.11. 2011,
> the results have been posted on 28.1.2012.
> 
> They reads as follows:
> Gold medal (600 points):
> Team "acl2-dkms": Jared Davis, Matt Kaufmann, J Strother Moore, and Sol Swords with ACL2.
> Team "KIV": Gidon Ernst, Gerhard Schellhorn, Kurt Stenzel, and Bogdan Tofan using KIV.
> Silver medal (595 points):
> Team "LeinoMueller": K. Rustan M. Leino and Peter Müller with Dafny.
> Team "SRI": Sam Owre and Natarajan Shankar using PVS.
> Bronze medal (590 points):
> Team "eam": Ernie Cohen and Michał Moskal with VCC.
> Team "JasonAndNadia": Jason Koenig and Nadia Polikarpova with Dafny.
> 
> 
> So, unfortunately, no Isabelle team made it among the top 6. 
> 
> Interestingly, both winning teams had 4 members and made several attempts to model and verify the same
> problem. Jay explained that they set up a telephone conference one hour after the opening of the competition,
> and then attacked various problems off-line, (besides the competition, all of them had other duties. Jay was,
> for example, attending a faculty meeting in the meantime ... ), joined regularly
> their results and rotated responsabilities for problems later on. In the late phase, the entire team
> concentrated on the remaining problems.
> 
> A look on the winning teams shows also that it helps to have an established team and tool chain
> (for imperative problems or not). The leading field was close - "eam" "lost" only because of a minor
> modeling problem in a precondition. 
> 
> The competition allowed even modifications of the tools during the competition; apparently
> no winning team made use of this option ...
> 
> Best regards,
> 
> bu
> 
>  
> 







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.