The 2024 New England Systems Verification Day will take place on Friday, April 26th, 2024, in room 45-801 in the Schwarzman College of Computing Building (building 45, 51 Vassar St., Cambridge, MA 02139).
| Time | Speaker | Topic |
|---|---|---|
| 08:00 AM | Breakfast available | |
| Verus | ||
| 09:00 AM - 09:20 AM | Jon Howell (VMware) | Verus: where it came from, what it can do, and why we think it can do those things |
| 09:20 AM - 09:40 AM | Travis Hance (CMU) | A concurrent memory allocator verified with Verus |
| 09:40 AM - 10:00 AM | Jay Lorch (MSR) | Verifying Azure storage with Verus |
| 10:00 AM - 10:20 AM | Upamanyu Sharma (MIT) | Distributed systems separation logic using Verus linear types |
| 10:20 AM - 10:50 AM | Break | |
| SMT | ||
| 10:50 AM - 11:10 AM | Andrea Lattuada (VMware) | Tunable automation for SMT-based verification in Verus |
| 11:10 AM - 11:30 AM | Yi Zhou (CMU) | Towards robust SMT-based automation in program verification |
| Low-level code | ||
| 11:30 AM - 11:35 AM | Sam Gruetter (MIT) | Live verification of C-like programs in Coq |
| 11:35 AM - 11:40 AM | Jiazheng Liu (MIT) | Modular verification of a programmable network switch |
| 11:40 AM - 12:00 PM | Gregory Malecha (Bedrock) | Specifying a hypervisor in separation logic |
| 12:00 PM - 01:00 PM | Lunch | |
| Compilers | ||
| 01:00 PM - 01:05 PM | Zhengyao Lin (CMU) | Verifying compilation to a reconfigurable dataflow architecture |
| 01:05 PM - 01:25 PM | Alexa VanHattum (Wellesley) | Verifying instruction selection in a WebAssembly-to-native compiler |
| Protocols | ||
| 01:25 PM - 01:45 PM | Simon Gregersen (NYU) | Trillium: separation logic for intensional refinement |
| 01:45 PM - 02:05 PM | Jianan Yao (Columbia) | Mostly automated verification of liveness properties for distributed protocols with ranking functions |
| 02:05 PM - 02:20 PM | Tony Zhang (Michigan) | Using invariant taxonomies to streamline distributed systems proofs |
| 02:20 PM - 02:25 PM | Bryant Curto (NEU) | Verifying safety and liveness of compositions of weakly consistent distributed systems |
| 02:25 PM - 02:30 PM | William Schultz (NEU) | Scalable, interpretable distributed protocol verification by inductive proof slicing |
| 02:30 PM - 03:00 PM | Break | |
| Cryptography | ||
| 03:00 PM - 03:20 PM | Pratap Singh (CMU) | Compiling security protocols from Owl to verified, high-assurance, performant implementations |
| 03:20 PM - 03:40 PM | Markus de Medeiros (NYU) | Error credits: resourceful reasoning about error bounds for higher-order probabilistic programs |
| 03:40 PM - 03:45 PM | Jon Aytac (Sandia) | Certified Cryptol interpreter in Coq for verifying post-quantum cryptography |
| 03:45 PM - 03:50 PM | Joshua Guttman (MITRE) | Cryptographically assured information flow: assured remote execution |
| Distributed systems | ||
| 03:50 PM - 03:55 PM | Derek Leung (MIT) | Modular verification of liveness for a PBFT implementation |
| 03:55 PM - 04:00 PM | Yun-Sheng Chang (MIT) | Verifying distributed sharded transactions using partially consistent replication |
| 04:00 PM - 04:20 PM | Longfei Qiu (Yale) | LiDO: linearizable Byzantine distributed objects with refinement-based liveness proofs |
| 04:20 PM - 04:50 PM | Break | |
| Hardware side-channels | ||
| 04:50 PM - 05:05 PM | Yuheng Yang (MIT) | Pensieve: microarchitectural modeling for security evaluation |
| 05:05 PM - 05:20 PM | Caroline Trippel (Stanford) | SynthLC: leakage functions from a SystemVerilog design |
| 05:20 PM - 05:35 PM | Cameron Wong (Harvard) | Collapsing towers for side-channel security |
| 05:35 PM - 05:55 PM | Anish Athalye (MIT) | Modular verification of non-leakage for hardware security modules with K2 |
| 05:55 PM - 06:00 PM | Murali Vijayaraghavan (Google) | Eliminating the security TCB using CHERI and Kami |
| 06:00 PM | Adjourn -- dinner on your own (we can suggest good places to go) | |
For 20-minute talk slots: please give a 15 minute talk, leaving 5 minutes for questions.
For 15-minute talk slots: please give a 10-minute talk, leaving 5 minutes for questions.
For 5-minute talk slots: please give a 5-minute-or-less talk, and take any substantial questions during the break.
Given the high number of talk proposals this year, we have a packed schedule, so please try to stick to the time limits. We will strictly enforce this.
For the talk, you should expect your audience to be verification experts.
We solicit talks about ongoing research in the area of systems verification. We are broadly interested in most topics in this space, but for some examples, take a look at the schedule from the workshops in 2017, 2018, 2019, 2021, and 2022.
Concretely, to propose a talk, send an email to Adam and Nickolai with one paragraph describing:
Full consideration will be given to proposals received by March 15th.
Thanks to Google and NSF for providing the funding for the food at this workshop.