~/talk

A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs

on YouTube 13m
Talkat OOPSLA 2021 · 2021-10-17..10-22· [software-architecture]

speakers

name:Paul He
links:none on file
name:Edwin Westbrook
links:none on file
name:Brent Carmer
links:none on file
name:Chris Phifer
links:none on file
name:Valentin Robert
links:none on file
name:Karl Smeltzer
links:none on file
name:Andrei Stefanescu
links:none on file
name:Aaron Tomb
links:none on file
name:Adam Wick
links:none on file
name:Matthew Yacavone
links:none on file
name:Steve Zdancewic
website:http://www.cis.upenn.edu/~stevez

resources

video:https://youtu.be/X6exz9CuqcU
slides:none on file

summary

A memory-safe Rust-like type system called Heapster typechecks LLVM IR and extracts Coq functions that represent imperative behavior without pointer reasoning, inserting dynamic checks in specs for array bounds and other safety-dependent operations. The Coq formalization proves semantic soundness: if the extracted spec cannot step to error then neither can the imperative program. Applied to an IPSec mbox implementation, the tool typechecks most functions, fails on four low-level ones, and lets the authors prove seven specs while also uncovering null-check and array-index bugs.

AI-written summary · about

chapters (4)

  1. 0:00Intro
  2. 2:38Project Overview
  3. 6:28Type Checking
  4. 9:04Semantic Typing

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.