Welcome to Unsound
summary
A new workshop establishes a venue to publish negative results about verification tools, cataloging concrete failures rather than vague caveats, and invites both formal logicians and hacky testers to submit reproducible breakages. It focuses on shared unsoundness patterns — bugs that recur across tools because of the same wrong assumptions — and on engineering tactics like model checking on top of verification tools and fast adversarial testing. Accepted work already includes exploiting known termination assumptions (Rubin Falls in arbitrary verification programs).
AI-written summary · about
chapters (7)
- 0:00Intro
- 0:28Verification
- 3:18Join us!
- 4:33Publishing negative results
- 6:18The new generations
- 7:56Welcome!
- 9:23Schedule
related talks
01h 00mWorkshop
31mSound Symbolic Execution via Abstract Interpretation and its Application to Sec...
20mSound Abstract Nonexploitability Analysis
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
16mTooling Design and Lessons Learned from Systematic Evaluations of the Preservation of(…)
10mClear as Mud
07mV for Verification
01h 15mMake your programs more reliable with Fuzzing