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.

• 10 Jan Organization meeting
• 17 Jan Group Town Hall
• 24 Jan Harshitha on Nagini
• 31 Jan Rocco on Atomic Conditions
• 7 Feb Oliver on Knuth-Bendix
• 14 Feb Manasij on Separation logic
• 21 Feb Cancelled (visit days)
• 28 Feb William on Serval
• 6 Mar Cancelled (spring break)
• 13 Mar Cancelled (spring break)

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