Email Gateway (Aug 18 2022 at 19:05): Email Gateway (Aug 18 2022 at 19:05):From: Johannes Hölzl <hoelzl@in.tum.de>
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
Email Gateway (Aug 18 2022 at 19:12):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
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
Last updated: Apr 20 2024 at 08:16 UTC