Work in Progress: Modelling Incorrect Programs in the Open World with D...
summary
Proposes using Dafny to model open‑world trust assumptions by adding an opaque ghost predicate (a “bay”) to pre/postconditions so specs explicitly record whether a component is trusted. Demonstrates a Box trait with invariant value>0 and two verified variants — good and evil Box implementations — where the evil one still assigns illegal values but verifies because the bay is false. Shows how Dafny’s ghost predicates plus optional runtime checks support gradual verification of partial systems.
AI-written summary · about
chapters (10)
- 0:00Modeling incorrect programs
- 1:05Open world in programming
- 3:59Trust and risk in specs
- 7:11Necessary vs sufficient specs
- 9:16Horizon scandal case study
- 12:51Circular specifications reasoning
- 13:56Daphne language for specs
- 16:03Ghost predicates for trust
- 19:20Untrusted dependencies modeling
- 20:02Q&A
related talks
32mPanel: Integrating Legend, Bosque, and Morphir For Open Reg Tech through FINOS
25mBad Behaviour: Automating System-level Safety Testing Using Open Source Tools
19mInterview
01h 30mTrustworthy AI & Open Source
18mBuilding pi in a World of Slop
13mAdvancing design verification with Verilator
51mPanel Discussion
47mBuilding Trust in Open Source: A Practical Guide to Securing Your ...