[Ufmrg] Fwd: [isabelle] Call for Participation: VerifyThis Long-Term Collaborative Challenge

Gergely Buday <g.buday@sheffield.ac.uk> Tue, 26 September 2023 13:15 UTC

MIME-Version: 1.0
References: <175f3cda-46be-4a20-a736-c6aa045a2e14@lmu.de>
In-Reply-To: <175f3cda-46be-4a20-a736-c6aa045a2e14@lmu.de>
From: Gergely Buday <g.buday@sheffield.ac.uk>
Date: Tue, 26 Sep 2023 14:15:17 +0100
Message-ID: <CAHgAKgSpwxWo2hkkF4n=k7i_SH3jGcLBdANaD9j9FRKYjtH3=Q@mail.gmail.com>
To: Ufmrg@irtf.org
Content-Type: multipart/alternative; boundary="000000000000688f30060642de4e"
Archived-At: <https://mailarchive.ietf.org/arch/msg/ufmrg/u_3oRY77_hxnaNdGObxUEWUkgQ4>
Subject: [Ufmrg] Fwd: [isabelle] Call for Participation: VerifyThis Long-Term Collaborative Challenge
Precedence: list

Dear Members,

this might be of interest to you, sorry if you have seen it already.

Yours

- Gergely

---------- Forwarded message ---------
From: Gidon Ernst <gidon.ernst@lmu.de>
Date: Tue, 26 Sept 2023 at 13:28
Subject: [isabelle] Call for Participation: VerifyThis Long-Term
Collaborative Challenge
To:


------------------------------------------------
   VerifyThis Collaborative Long-Term Challenge
             Call for Participation

   Next Event: November 14 at iFM 2023, Leiden
      The Netherlands (details see below)

          https://verifythis.github.io/
https://liacs.leidenuniv.nl/~bonsanguemm/ifm23/
------------------------------------------------

The VerifyThis Collaborative Long-Term Challenge aims to to demonstrate
practical value of formal methods, to evaluate the current tools on
specifying and verifying requirements of realistic software systems, and
to bring together the community for an exchange on the state-of-the-art
and future directions.

An emphasis is placed on encouraging collaboration between participating
research groups,not just at a conceptual level but also towards
integrating verification tools and approaches, e.g., sharing technical
artifacts such as specifications and proofs.

Challenge Description: https://verifythis.github.io/03memcached/
Slides: https://verifythis.github.io/03memcached/slides_etaps23.pdf
Reference System: http://memcached.org

The ongoing challenge is dedicated to Memcached, a key-value cache
server. Memcached is the backbone for fast response times in distributed
web-application. The goal is not only to provide an investigation on the
server alone, but also take the client-side and the protocol into
consideration. The challenge covers a wide range of requirements and is
therefore suited for different approaches and verification tools, such
as model-checking, static analysis, and deductive techniques. We welcome
all kinds of contributions from high-level specifications down to models
down code-level analysis.

Please announce your participation on the Mailing List:
verifythis-ltc@lists.kit.edu We encourage you to actively reach out for
collaboration!

**Next Event: **
We are pleased to announce that a  full session at iFM 2023 will be
dedicated to a public discussion of the challenge. In this session, we
will give a short overview of the Long-Term Challenge, complemented by
lightning talks to stimulate an interactive discussion to foster further
activities. Therefore, we invite all interested researchers to join the
session - no additional registration is necessary.

If you have any questions, feel free to contact the organizers.

Gidon Ernst
Alexander Weigl

[Ufmrg] Fwd: [isabelle] Call for Participation: V… Gergely Buday