Unsound 2022
| title | author | length |
|---|---|---|
| Welcome to Unsound | 11m | |
A new workshop establishes a venue to publish negative results about verification tools, cataloging concrete failures rather than vague caveats, and invites… | ||
| What do we mean by "unsound"? | Jan Bessai | 45m |
Defines unsound model as one that validates a formula but fails when interpreted into the real system, giving concrete examples: reference-semantics models… | ||
| How to trust a verified program? | Wouter Swierstra | 47m |
Proof assistants like Agda, Coq and Lean still permit real failures: a universe overflow caused by 63-bit integer wrap lets Agda accept falsity; a… | ||
| MetaCoq as a tool to prevent future unsoundness in Coq | Yannick Forster | 42m |
MetaCoq formalizes Coq’s calculus inside Coq and provides verified implementations of core pieces of the kernel, aiming to catch soundness bugs before they… | ||
| Proving False in Object Oriented Verification Programs by Exploiting Non-Termination | Jaymon Furniss | 24m |
Three small programs show Gobra, KeY, and Dafny producing proofs of false by hiding non-terminating proofs in ghost variables and then compiling only the… | ||
| The 4 horsemen of unsoundness in OO languages | Marco Servetto | 49m |
Four concrete pitfalls: a pair of independently verified implementations that call each other via an interface produce nontermination despite each being marked… | ||
| Discussion | 25m | |
Group discusses concrete next steps to run Unsound yearly or biennially and form a standing program committee, plus specific outreach targets: verified… | ||
| nothing matches | ||