coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "r.e.monti AT utwente.nl" <r.e.monti AT utwente.nl>
- To: "verifythis-ltc AT lists.kit.edu" <verifythis-ltc AT lists.kit.edu>, "jmlspecs-interest AT lists.sourceforge.net" <jmlspecs-interest AT lists.sourceforge.net>, "concurrency AT listserver.tue.nl" <concurrency AT listserver.tue.nl>, "types-announce AT LISTS.SEAS.UPENN.EDU" <types-announce AT LISTS.SEAS.UPENN.EDU>, "SEWORLD AT SIGSOFT.ORG" <SEWORLD AT SIGSOFT.ORG>, "coq-club AT inria.fr" <coq-club AT inria.fr>, "ipalist AT listserver.tue.nl" <ipalist AT listserver.tue.nl>
- Subject: [Coq-Club] VTLTC 2020 - Call for Online Participation
- Date: Wed, 8 Apr 2020 09:36:59 +0000
- Accept-language: en-US, en-GB
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=r.e.monti AT utwente.nl; spf=Pass smtp.mailfrom=r.e.monti AT utwente.nl; spf=None smtp.helo=postmaster AT out49-ams.mf.surf.net
- Ironport-phdr: 9a23:/3IFhBChmIVC2Z8VAdDVUyQJP3N1i/DPJgcQr6AfoPdwSP3/p8SwAkXT6L1XgUPTWs2DsrQY0reQ6v+rADNIoc7Y9ixbLNoUD15NoP5VtjJjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMjoZuN6Y8xgHUrnZKdOha2GFlLk+Xkxrg+8u85pFu/zlftv4768JMTaD2dLkkQLJFCzgrL2866Mr3uBfZUACB/GEcUmIYkhpJBwjK8hT3VYrvvyX5q+RwxjCUMdX5Qr4oVzui6bxrSALzhyccKzE56mDXhddug69dvRmsugZww4/QYIGSKfp+YqbQds4USGZdQspcUTFKDYShYYsSFOoBJfhXoJXhp1UAqhu+ABOjBOLpyjRVgnP70qk33+EnHArb3gIvAsgOvWzUotvrKakSTe67wqrJzTrfYPxbwi3y5JTNch07vf2AQbB9fMzMwkcvDQPFiVCQpJTrMzOPzOgCrXKX7+9nVeKpl24nqhp8oiWzxsYilIbJgJ4VxU7e+SV/xIY5K8CzRUlhYdK+DpRcrSSaN4xwQsM+QmFlozs6yqEIuJGleigK1IooywTZa/yDaoWF5A/oWuiWITd9nn1lebS/ig698Uih1u38VtS0301QoipEldnArmwN1x3W6seZUPR9+Fqu1iuV2ADP9O5IO1w7la3eK5I53LEwipoTsEXZEiDqmEX6lLSWeVs9+ui17OTnY6/pqoaEN497kgHyKKMumtawAek+LwMAXHCb9Pyh2LDs/UD1WqlGgucrnqXDv53XIdwXqrO3DgNJyIou6BKyAy2i3dgCg3UKIlFIdAqJj4f3OFzCPPX1APK8jlmvjjtk2vXLMaPhD5jNMnTOlanucahm5ENfzQc80MxT6pNJBbwHPfn9QFX+tMbCAR88KwG0w/joCNF61o4GXmKPH7OZPazWvFOR/O0vJvKMaJUQuDbzMfQl/OPujWU3mVMHe6mmw4cXZGi5HvRgPUqZfWLhjsoOHGoKpAYyUPbmhECYXTNcY3u+R6c86Ss6CIKiA4fDXIetgLmZ0SehBJFZeHpKClWLEXfua4WEWuwBaD+OIs5vjDMEU6ShRJE72RGosA/206BnIfbM+i0EqZLj08B46PHUlREr7DB7E8Cd03yWQGxvhWMJRzo23LhlrkBny1eD17J4g/1CGtBJ6fNJSFRyCZmJhfJ3EdH8Sx7Bf8zMTEqtatGnGi0qCNEw35kDb1s3U4G8gwrC0Tu2A74O0riXD7Qw87nAxD7yJto7xnrbgu1pxVsjRtBXOGa9w6956wXJCpXVu0GYjLqxM78bwTTG+WmE12WD+kdVTEQ4BafAWWsHa0DN6NX/+k7YQqSyIbAmKRdaj9WFN7FBZ9Pul1pLAvHuJIKaKyi6nGG7GAySy7WHfaLuen4BxyjHFkUe1RwO8DCAMUJ2UiympWnDFiZjE1n+S0ft6vVlpWmlQ1Vy0xyHKUtlgf79sAIEnfGHDvoV2LUZviwsgxFVJ2qGmen7IuHGmjJMWoMaTP8Aqh8TyXPBuhc4N5qmKL1kjVM2VyVMg3io7DheMcN9qeUMijUH4DckberS635+UAm88bjLG5LsDUfOujeVROSejmrz7/Gs3osn09UXkHLNgEeOLGV0tz0t2N5MlnCY+5/iDQwIUJu3XFx9v0xxoKifaS0g7avV02dtOO+6qGmGk5goHOIhyw28V9NeK7+fGRXsHtdcG9Wjbuou0RD9bwoNOOFJ6IYwPti6bPacxqOxevp9kXSgiTIUzpp61xfG7WxxDOvP2YoE6+yEwQaBSzq6ilPr+pTt340CYDYUAmuX1DT7CYhNa+t0edBYWi+VP8Sry4Am1NbWUHlC+Qv/VgpXiv/sQgKbahnG5SMV0E0WpXK9ni7hlW5pjy4kqLaSmirKkb27KUg3f1VTTWwntm/CZIi5i9dABxqvchR1xV6s4F28wqYdv7llIS/VTFsaJ3GqfVEnabO5s/+5W+AK8Ikh6H8FTfijbFaGR/j7p0lC3g==
Call for Online Participation.
VerifyThis Long-Term Challenge 2020
-- Online Result and Exchange Event --
27th April 2020, 10:00 UTC [0]
>>> https://verifythis.github.io/online-event <<<
## Introduction
The VerifyThis Long-Term Challenge complements the on-site format of the VerifyThis competition with a verification challenge, in which teams contribute to the verification of a practically relevant piece of software over a longer period of time. The challenge aims to be a showcase that deductive program verification can produce relevant results for real systems with acceptable effort.
The challenge system to be verified is the new implementation of the PGP server infrastructure, called HAGRID [2]. The old implementation did not conform to GDPR and was known to be vulnerable against DoS attacks.
## The Online Result and Exchange Workshop
A final workshop session for the challenge had been planned at ETAPS (along with the VerifyThis program verification competition [1]). Since ETAPS has been postponed, we will meet and exchange online.
We have received five submissions that each contribute a solution to different aspects of the challenge using different abstractions, different assumptions and different verification techniques.
During this online meeting, the different solutions will be briefly explained, and we discuss the approaches, how they can benefit from one another and how further verification success can be stipulated.
This meeting is not meant as a replacement of the on-site event. It is meant as an informal event to exchange ideas, to give positive impulses on further advances of approaches, or on how to combine solutions. If the situation permits, the onsite event will take place in autumn during ETAPS.
## Call for Participation
Everybody who is interested about the challenge, the proposed solutions and VerifyThis is cordially invited to join the meeting!
## Online Link
More information on how to participate, agenda and resources are on our webpage of the online workshop:
>>> https://verifythis.github.io/online-event <<<
## Program Chairs and Organizers
Marieke Huisman Raul E. Monti
Mattias Ulbrich Alexander Weigl
[0] Find out your local time here: https://www.timeanddate.com/worldclock/fixedtime.html?msg=VerifyThis&iso=2020-04-27T10:00:00
[1] https://www.pm.inf.ethz.ch/research/verifythis.html
[2] https://sequoia-pgp.org/blog/2019/06/14/20190614-hagrid/ |
- [Coq-Club] VTLTC 2020 - Call for Online Participation, r.e.monti AT utwente.nl, 04/08/2020
Archive powered by MHonArc 2.6.18.