Campus Event Calendar
Event Entry
What and Who
Foundational Verification of Low-Level Code: RefinedC and Beyond
Deepak Garg
Max Planck Institute for Software Systems
Joint Lecture Series
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 3 July 2024
12:15
60 Minutes
E1 5
002
Saarbrücken
Abstract
Low-level code written in languages like C forms the bedrock of most computer systems today. Establishing the correctness of this code is important for the safety and security of our systems. The gold standard for code correctness is foundational verification -- the construction of mathematical proofs of program correctness verified in a proof assistant like Coq. However, foundational verification of low-level code is a tedious task that has, so far, largely relied on adapting code to suit the constraints of the verification framework, e.g., the programming idioms that are supported.
In this talk, I will present RefinedC, a new Coq-based C verification framework that aims to address the above limitation. By design, RefinedC is foundational (all proofs are mechanically verified within Coq), extensible (it can be extended to support new program properties, programming idioms and even new languages) and automation-friendly. Time permitting, I will also discuss projects that extend RefinedC's capabilities to reason about code written in other low-level languages like assembly, and code written in more than one language.
(This talk is based on joint work with several other research groups, notably the group of Derek Dreyer at MPI-SWS.)
Contact
Jennifer Müller
+49 681 9325 2900
--email hidden
Virtual Meeting Details
Zoom
997 1565 5535
passcode not visible
logged in users only
Jennifer Müller, 06/26/2024 10:25 -- Created document.