# 07/25/25: RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types with Michael Sammler

Page: 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
Text version: 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
Podcast: [Boston Computation Club](https://stenobird.com/podcast/boston-computation-club-4031660)
Published: 2025-07-25T16:29:49+00:00
Episode link: https://podcasters.spotify.com/pod/show/bostoncc/episodes/072525-RefinedC-Automating-the-Foundational-Verification-of-C-Code-with-Refined-Ownership-Types-with-Michael-Sammler-e360vsb
Audio file: https://anchor.fm/s/5eee01ac/podcast/play/105987403/https%3A%2F%2Fd3ctxlq1ktw2nl.cloudfront.net%2Fstaging%2F2025-6-25%2Fc59495f0-5032-8b1f-6cab-dc7c16c44a91.m4a
Processing state: not_requested
JSON: 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
Duration seconds: 3120

## Resource

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!

## Actions

- request_transcript: `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.
- read_markdown: `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.

A page view does not enqueue transcription. Agents should invoke `request_transcript` explicitly when they need this episode processed.

## Transcript

Full transcripts are not published on public pages unless there is a clear rights basis.