Samuel Gruetter is a final-year PhD student in Computer Science at MIT in Adam Chlipala's group, working on formal verification of software using the Coq proof assistant.Prior to MIT, Samuel received a Bachelor's and Master's at EPFL in Lausanne, Switzerland where he was a student research assistant in Martin Odersky's Scala lab, working on the theoretical foundations of the Scala language. He did a Master's project internship at Princeton University with Andrew Appel's group, working on their Verified Software Toolchain, and also worked at the University of Melbourne, Australia, with Toby Murray on information flow proofs for C programs. Website: https://samuelgruetter.net/

SWS   Info

AG Audience

English

60 Minutes

Saarbrücken

I will present a framework that makes it easier to write correctness proofs for programs written in Bedrock2, a small subset of C. The user can write the program and the proof at the same time, and the Coq proof assistant serves as a kind of symbolic debugger, presenting in real-time a concise summary of all the facts it knows about the current symbolic state of the program. I'm also exploring an interesting middle-ground between manually spelled out loop invariants and automatically inferred loop invariants: Since the symbolic state before a loop often is quite similar to the loop invariant, I only require the user to express the diff between the two as a tactic script, which tends to be more concise and more maintainable than a manually spelled out loop invariant. PLDI'24 Paper: https://dl.acm.org/doi/10.1145/3656439

Lena Schneider

+49 681 9303 9107

--email hidden

Zoom

966 8141 4048

passcode not visible

logged in users only