Listen "07/25/25: RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types with Michael Sammler"
Episode Synopsis
Michael Sammlern assistant professor leading the Programming Languages and Verification Group at the Institute of Science and Technology Austria (ISTA). Today he joined us to talk about his three primary projects: RefinedC, which uses a refinement and ownership type system to verify C code, Islaris, which shows how to scale verification of assembly code to realistic models of real-world architectures, and DimSum, which provides a decentralized approach for reasoning about multi-language programs (with a particular focus on RefinedC). We had a small but really dedicated crowd which facilitated an excellent discussion. This was a really fun one and we hope you enjoy it as much as we did!
More episodes of the podcast Boston Computation Club
08/15/25: An LLM Agent for Functional Bug Detection in Network Protocols with Mingwei Zheng
15/08/2025
08/01/25: Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification with Kaiyu Yang
02/08/2025
ZARZA We are Zarza, the prestigious firm behind major projects in information technology.