The 2025 New England Systems Verification Day will take place on Friday, October 3rd, 2025, 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 | |
| Verifying existing software | ||
| 09:00 AM - 09:20 AM | Upamanyu Sharma (MIT) | Verifying real-world distributed systems code using Grove |
| 09:20 AM - 09:40 AM | Elanor Tang (CMU) | Verifying the Rust Standard Library Using Verus |
| 09:40 AM - 10:00 AM | Levi Redlin (Wisconsin) | Verifying Go code with channels in Goose and Perennial |
| 10:00 AM - 10:30 AM | Break | |
| Automation | ||
| 10:30 AM - 10:45 AM | Armin Vakil (Michigan) | Synthesizing Safety Proofs Using Triggers |
| 10:45 AM - 11:00 AM | Can Cebeci (EPFL) | Building a stable verifier for systems code without sacrificing automation |
| 11:00 AM - 11:15 AM | Max Tegmark (MIT) | ML-techniques for making formal verification faster and cheaper, and on program synthesis of proof-carrying code |
| Verification infrastructure | ||
| 11:15 AM - 11:30 AM | Ankush Das (BU) | Nested permissions for disjointness reasoning |
| 11:30 AM - 11:50 AM | Dustin Jamner (MIT) | Verifying e-graphs in Rocq |
| 11:50 AM - 12:10 PM | Zichen Zhang (NYU) | Building Extensible Program Logics with Effect Handlers |
| 12:10 PM - 01:10 PM | Lunch | |
| Distributed systems | ||
| 01:10 PM - 01:25 PM | Longfei Qiu (Yale) | LiDO-DAG: A Framework for Verifying Safe and Liveness of DAG-based Consensus Protocols |
| 01:25 PM - 01:40 PM | Derek Leung (MIT) | Proving liveness of distributed systems with Byzantine participants |
| 01:40 PM - 01:55 PM | Bryant Curto (Northeastern) | Compositional Model-Driven Verification of Weakly Consistent Distributed Systems |
| 01:55 PM - 02:10 PM | Yun-Sheng Chang (MIT) | Modular verification of distributed transactions using locally inconsistent partitions |
| 02:10 PM - 02:25 PM | Baltasar Dinis (MIT) | Verifying distributed systems in Verus |
| 02:25 PM - 02:55 PM | Break | |
| Cryptographic systems | ||
| 02:55 PM - 03:10 PM | Vilhelm Sjoberg (CertiK) | Formal Verification of zkWasm, a General-Purpose zkVM |
| 03:10 PM - 03:25 PM | Simon Gregersen (NYU) | Logical Relations for Formally Verified Authenticated Data Structures |
| 03:25 PM - 03:40 PM | David Holland (Galois) | Verifying Rust Smart Contracts with SAW and Cryptol |
| 03:40 PM - 03:55 PM | Shixin Song and Tingzhen Dong (MIT) | Securing Cryptographic Software via Typed Assembly Language and a Hardware Extension |
| 03:55 PM - 04:10 PM | Sanjit Bhat (MIT) | Verifying a key-transparency system implementation |
| 04:10 PM - 04:40 PM | Break | |
| Hardware and performance | ||
| 04:40 PM - 04:55 PM | Amanda Liu (MIT) | Verified scheduling framework for optimizing high-level tensor programs |
| 04:55 PM - 05:10 PM | Murali Vijayaraghavan (Google) | Rigorous Hardware-Software Codesign for Secure Compartmentalization on Embedded Devices |
| 05:10 PM - 05:25 PM | Pranav Srinivasan (Michigan) | TakoFormal: Enabling Robust Software for Programmable Memory Hierarchies |
| 05:25 PM - 05:40 PM | Yatin Manerkar (Michigan) | PipeSketch: Automated Microarchitectural Model Generation Through Programming by Demonstration |
| 05:40 PM - 05:55 PM | Yi Cai (UMD) | Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust |
| Miscellaneous | ||
| 05:55 PM - 06:10 PM | Vadim Zaliva (Tufts) | Fault Flow Analysis and Verification with Typestate and Predicate Guards |
| 06:10 PM - 06:15 PM | Zekai Li (Brown) | Rt: a new type system for the streaming shell based on regular languages |
| 06:15 PM | Adjourn -- dinner on your own (we can suggest good places to go) | |
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.
Please leave 5 minutes for questions at the end of your talk slot; subsequent questions can be discussed during the coffee breaks. (For 5-minute slots, you don't need to leave time for questions.)
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, 2022, and 2024.
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 August 15th.
Thanks to Google and NSF for providing the funding for the food at this workshop.