CPU logo

Software Correctness Seminar covers major developments in formal verification, program analysis, and synthesis. We meet every Friday at 11:00 in the LCR. Join the mailing list for email updates.

Seminar is cancelled for the remainder of term due to the coronavirus.

Carry-over: Verifying Message Passing, Deterministic Reductions

Ganesh’s Proposals: Bit-width-independent SMT, Automating Separation Logic Using SMT, Separation logic with linked lists, FlyMC

Pavel’s Proposals: General deforestation, MetaLibm, Session Types, Next 700 Semantics, JS Inline Caches

Previous Interations: Fall 2019, Spring 2009