[isabelle] The VSTTE'12 Modeling and Verification Competition



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.