Episode
07/25/25: RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types with Michael Sammler
- Podcast
- Boston Computation Club
- Published
- Jul 25, 2025
- Duration seconds
- 3120
- Processing state
not_requested
Actions
POST https://stenobird.com/v1/public/podcasts/boston-computation-club-4031660/episodes/07-25-25-refinedc-automating-the-foundational-verification-of-c-code-with-refined-ownership-types-with-michael-sammler/transcription-requests
Idempotently request low-priority transcript generation for this episode.GET https://stenobird.com/podcast/boston-computation-club-4031660/07-25-25-refinedc-automating-the-foundational-verification-of-c-code-with-refined-ownership-types-with-michael-sammler.md
Read the agent-friendly Markdown representation of this episode resource.
Summary
Michael Sammler n 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!