Automated Verification of Parametric Channel-Based Process Communication
summary
A toolchain named Ginger translates Go fragments into a compact core language Virgo, encodes them as Hoare triples and checks partial-deadlock freedom using the Dafny verifier; it infers concurrency preconditions when universal safety fails. On a real-world corpus of 583 parametric fragments it models, 378 are expressible in Virgo, 145 are fully verified for all inputs, and 228 yield nontrivial inferred preconditions; the implementation and artifacts are available on GitHub.
AI-written summary · about
chapters (6)
- 0:00Go concurrency and deadlocks
- 3:55Parametric channel deadlocks
- 6:03Ginger tool overview
- 9:16Deadlock-free verification strategies
- 12:10Ginger evaluation on Uber codebase
- 12:58Q&A
related talks
20mNegative/Positive Verification for WorldGuard, CHERI and Other RISC-V Security Models-
21mCombined Dynamic and Formal Verification Approach to Processor Verification
14mMultiparty GV: Functional Multiparty Session Types with Certified Deadlock Fre...
18mPreview: Verification (Correctness)
22mOpen source design testing and verification with UVM and Verilator
38mThe Verification of a Distributed System
32mCorrectness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
23mOpen Source Verification Platform for RISC V Processors