VerifyThis Long-Term Challenge


Formal Verification of Real-World Software

What is VerifyThis?

The VerifyThis verification competition is a regular event run as an onsite meeting with workshop character in which three challenges are proposed that participants have to verify in 90 minutes each using their favourite program verification tool.

Related Event: VerifyThis On-site competition

We have experienced that the state of the art of program verification allows the participants to specify and verify impressively complex algorithms in this short a time span. If such sophisticated, realistic but not real, problems can be solved in real-time, what would be achievable if (a) we as the program verification community collaborated and (b) the time constraints were removed?

The Memcached Challenge

VerifyThis Long-Term Challenge aims at proving that deductive program verification can produce relevant results for real systems with acceptable effort on a large scale in a collaborative manner.

The current challenge is dedicated memcached, a simple LRU-cache based key-value 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 our considerations.

How to participate?

Participation on the challenge is easy. You should pick your favourite tool for the formal software assessment, and try whether you find a bug or prove adhering of the specification in HAGRID (or a suitable abstraction). Of course you can participate in groups. Moreover, we would like to foster collaboration between participating groups. Therefor we would appreciate if you register your group. Do not forget to also subscribe to our mailing list (verifythis-ltc@lists.kit.edu) to be able to share your questions and your work and to keep up to date with the work of the rest of the teams.

We plan to go for a Track on ISoLA 2024. In the intermediate, we plan rather informal meetings on iFM'23 and ETAPS'24.

News

Contract Languages I: Alessandro Cimatti: Software Contracts meet System Contracts – 15 May 2024

As a follow-up to the March 2024 Lorentz Center workshop on Contract Languages, we will host a series of online presentations and discussions around formal methods with contract languages, aligning with the LTC goal of enabling information exchange between different formal systems.

The first presentation was given by Alessandro Cimatti on “Software Contracts meet System Contracts”.

The [slides] of this presentation are available.

Next Meeting: 23 January 2024

The next discussion meeting will be on 23 January 2024, 10.00 CET.

Program

  • Presentation by Aurel Bílý on their approach using Prusti
  • Technical Discussions
  • Collaboration and Follow-up

Registration: Please sign up on the mailing list, we will post the Zoom link shortly before the meeting; alternatively send an E-Mail directly to the organizers.

More Information

Memcached Challenge

The second challenge will be disclosed at the ETAPS on Wed, 26th April 2023.

The introduction is scheduled in the TOOLympics session.