Verify This: Memcached-A Practical Long-Term Challenge for the Integration of Formal Methods

Challenging benchmarks are a major driver for sharpening our tools and theories. This paper introduces the second VerifyThis long-term challenge: The specification and verification of a remote key-value cache, inspired by and acting as compatible drop-in replacement of the memcached software package, which is widely used in industry. We identify open gaps in the formal specification and verification of systems. Goal of the challenge is therefore to foster collaboration in order to advance the capabilities of current methods and also to verify a realistic and industrially-relevant software application. This challenge has it all: high-level modeling of communication protocols, intricate algorithms and data structure, code level verification, safety and liveness properties as well as security challenges. It emphasizes the opportunity and need to integrate approaches and tools across the entire spectrum of formal methods. Website: https://verifythis.github.io/ Mailing List: https://www.lists.kit.edu/sympa/info/verifythis-ltc Reference System: http://memcached.org/