Discussion
summary
Group discusses concrete next steps to run Unsound yearly or biennially and form a standing program committee, plus specific outreach targets: verified compiler people, Iris users, Daphne adopters. Debate centers on provable failures: Java/Scala initialization bugs, examples that break contracts via subtyping, and whether step-indexing as a partial fix or Scala initialization checker actually resolves them. Practical risks include perverse incentives in industry and attackers slipping verified-but-broken code into real projects.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 3:31Organizing verification community
- 5:18Venue and inclusivity
- 7:01Perverse incentives
- 10:39Reporting unsoundness
- 14:09Verification tool challenges
- 15:57Automation vs foundational work
- 17:01Tool limitations
- 18:27Q&A
related talks
17mDiscussion - Protocols, Session 2
10mClear as Mud
01h 35mSafety and Security for C++: Panel Discussion
27mSecurity: The Thing That Everyone...
41mBattle of the Languages
12mWelcome and Overview
01h 07mPanel Discussion: What is Lacking in Linux Security and What Are or Should We be Doing about This
36mBoF
