A foundational platform for fully-formally-verified systems design
Events
13th - 14th April 2026: Rust Verification Workshop, co-located with ETAPS 2026, Turin Link to event
27th - 29th April 2026: Meilensteinsymposium EvIT, Halle
24th July 2026: Workshop on the Ergonomics of Verification Interfaces & Tools (EVIT Workshop), co-located with CAV 2026, Lisbon Link to event
22th - 25th September 2026: Informatik Festival 2026: Forum on Specification-driven Formal Verification, Dresden Link to event
Publications
WP-Preserving Compilation -- Preserving Weakest Preconditions for End-to-End Verification
presented at 53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026) in Rennes, France
Authors: Dr. Carmine Abate, Mohamed Elsheikh, Kleio Liotati, Dr. František Farka, Dr. Sebastian Ertel
Abstract: Systems are usually implemented in a high-level language, compiled to machine instructions and run on a dedicated hardware architecture. The goal of end-to-end verification is to prove a system meets its intended specification at the high-level language, and preserve such a property across the lower, more concrete layers, all the way down to the hardware. Large scale end-to-end verification of a system therefore requires:
- A program logic for the language in which the system is implemented.
- A compilation chain that preserves properties of the system from the high-level source language down to the target language, e.g., machine code.
We propose a strategy for end-to-end verification based on a compilation chain that preserves the properties provable in a weakest precondition calculus for the source language.
Debug, Execute, Verifiy! Development-Verification Co-Design Made Pratical
presented at the 13th workshop on Programming Languages and Operating Systems (PLOS 2025) in Seoul, South Korea
Authors: Dr. František Farka, Dr. Carmine Abate, Dr. Shuanglong Kan, Dr. Sebastian Ertel
Abstract: To formally verify large-scale systems, development and verification needs to be tightly integrated right from the start but this requires tool support that is currently missing. We present a framework for the Rust programming language that utilizes symbolic program execution to bridge the gap between development and verification. A use case provides first evidence that our tool integrates formal verification into the early development cycle and thus has the potential to scale for the verification of large systems.