Re: [isabelle] Proving Contests
- To: José Manuel Rodriguez Caballero <josephcmac at gmail.com>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>
- Subject: Re: [isabelle] Proving Contests
- From: Gidon Ernst <gidon.ernst at unimelb.edu.au>
- Date: Wed, 7 Nov 2018 02:26:17 +0000
- Accept-language: en-US
- In-reply-to: <CAA8xVUhm=WwPsCEfwgrzGwdxcoN7hhV2metf0mYK+c2yDGdMYQ@mail.gmail.com>
- References: <CANQq8HWwTaAOppm7rKGbDJVuu-mzP15RCkKHxDsPZwydL7Uy=A@mail.gmail.com>, <CAA8xVUhm=WwPsCEfwgrzGwdxcoN7hhV2metf0mYK+c2yDGdMYQ@mail.gmail.com>
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
- Thread-index: AQHUdi5MOsYas3WPWU6l0Ozq6UpOdaVDkyvM
- Thread-topic: [isabelle] Proving Contests
two similar competitions come to mind:
1st and 2nd VSComp, see
The 1st verified software competition: Experience report, FM2011
The 2nd verified software competition: Experience report, COMPARE 2012
VerifyThis (yearly at ETAPS)
This year, the Isabelle Team from TUM took the gold medal :)
Huisman, Klebanov, Monahan: On the organisation of program verification competitions, COMPARE 2012
the yearly competition reports, and the STTT 17(6) special issue: https://link.springer.com/journal/10009/17/6/page/1
Hope you find this information useful :)
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of José Manuel Rodriguez Caballero <josephcmac at gmail.com>
Sent: Wednesday, November 7, 2018 10:59:06 AM
To: cl-isabelle-users at lists.cam.ac.uk
Subject: [isabelle] Proving Contests
> max wrote:
> Just now we anounced the contest system,
> which we are using for managing homework submissions for
> the current Semantics course here at TUM, as well as providing
> a (short) tutorial to Isabelle and the system.
> Also, we host monthly contests with relatively easy but hopefully
> fun problems. I'm already looking for problems for the month of
> December. I think the goal should be that experienced Isabelle
> users can solve them within 30 minutes.
Nice project. My idea of an International Olympiad in Isabelle are a little
bit different. Indeed, I can summarize my vision as follows:
1) There will be some publicity about the International Olympiad some
months before its date. The publicity should be mainly addressed to
undergraduate and high school students. People interested in the Olympiad
should summit their email addresses in a website. People working with
Isabelle in an official research project, e.g., a Master, a PhD, a
professor or a professional programmer, are not allowed to apply in order
to guarantee more space for beginners.
2) The day of the Olympiad, a thy-file with a theorem followed by sorry
will be sent to each one of the email addresses.
3) People can submit their solutions until 6 hours after their received the
email with the problem (5 hours to solve the problem and 1 hour to make a
break, I guess). Solutions sent after the deadline will be automatically
4) An automatic system (software) will discriminate the invalid solutions,
e.g., using sorry somewhere, from the valid solutions. After that, it will
make an ordering according to the running time of each valid solution.
5) Finally, an email with the ranking of his/her solution will be
automatically sent to each participant. The participants having ranking 1,
2, 3 will receive a prize.
When I think about such an international project, I am mainly concerned
with people living in economically less developed countries. The idea is
that a person from such countries, having the dream of winning an
International Olympiad in Isabelle will have a motivation to improve
himself/herself in this field. Of course, classification by countries
should be avoided and people from highly developed countries should be
allowed to participate as well.
This is just a dream, I have not enough free time to do something about it.
My inspiration are the IOI: https://ioinformatics.org/
This archive was generated by a fusion of
Pipermail (Mailman edition) and