The 2022 New England Systems Verification Day will take place on Friday, October 28th, 2022, in room 32-G449 ("Kiva") at the Stata Center (32 Vassar St, Cambridge, MA 02139).
The building is open during the day, but the elevator requires card access (leftover from Covid protocols), to go up to the 4th floor. We will have volunteers escorting attendees from the first floor of the Gates tower to the workshop on the 4th floor, between 8am and 9am. (We may even manage to get the relevant door kept unlocked on that day.) If you get stuck, send an email to Adam and Nickolai and we'll come get you.
| Time | Speaker | Topic |
|---|---|---|
| 08:00 AM | Breakfast available | |
| Hardware / software | ||
| 09:00 AM - 09:20 AM | Anish Athalye (MIT) | Knox: Verifying Hardware Security Modules |
| 09:20 AM - 09:40 AM | Andres Erbsen (MIT) | Deriving a microcontroller-compatible crypto library and application |
| 09:40 AM - 09:55 AM | Drew Zagieboylo (Cornell) | PDL: Hardware Design Language for Pipelined Processors |
| 09:55 AM - 10:25 AM | Break | |
| Distributed systems | ||
| 10:25 AM - 10:45 AM | Upamanyu Sharma (MIT) | Grove: Verifying Recoverable Distributed Systems |
| 10:45 AM - 11:05 AM | Zhong Shao (Yale) | Adore: Atomic Distributed Objects with Certified Reconfiguration |
| 11:05 AM - 11:20 AM | Max von Hippel and Ankit Kumar (NEU) | Formal Analysis of Ethereum's GossipSub in ACL2s |
| 11:20 AM - 11:35 AM | Armin Vakil (Michigan) | Automatically fixing proofs and protocols |
| 11:35 AM - 11:40 AM | Derek Leung (MIT) | Verifying liveness for Byzantine fault tolerance |
| 11:40 AM - 11:45 AM | Jianan Yao and Ronghui Gu (Columbia) | Inductive Invariant Inference in DuoAI |
| 11:45 AM - 11:50 AM | Will Schultz (NEU) | Inductive Invariant Inference in TLA+ |
| 11:50 AM - 12:50 PM | Lunch | |
| Low-level systems | ||
| 12:50 PM - 01:10 PM | Jasper Haag (BedRock Systems) | Verifying C++ at BedRock Systems using BRiCk |
| 01:10 PM - 01:30 PM | Travis Hance (CMU) | Seagull: Automated Modular Reasoning for Complex Concurrent Systems |
| 01:30 PM - 01:45 PM | Xupeng Li and Ronghui Gu (Columbia) | Design and Verification of Armv9 CCA |
| 01:45 PM - 02:00 PM | Vadim Zaliva (Digamma.ai) | Formal verification of ASN.1 and Coreboot SMI |
| Security | ||
| 02:00 PM - 02:15 PM | Evan Johnson (UCSD) | WaVe, a verified secure runtime system for WASI in WASM |
| 02:15 PM - 02:20 PM | Atalay Ileri (MIT) | Confidentiality under nondeterminism |
| 02:20 PM - 02:25 PM | Paul Crews (Google) | Defining recoverability for arbitrary security properties |
| 02:25 PM - 02:55 PM | Break | |
| Crypto protocols | ||
| 02:55 PM - 03:15 PM | Joshua Gancher (CMU) | End-to-End Verification for Security Protocols |
| 03:15 PM - 03:30 PM | Arthur Azevedo de Amorim (BU) | Cryptis: Cryptographic Reasoning in Separation Logic |
| 03:30 PM - 03:45 PM | Jonathan Protzenko (MSR) | Noise* protocol compiler |
| 03:45 PM - 04:00 PM | Josh Acay (Cornell) | Verifying the Viaduct distributed cryptographic compiler |
| 04:00 PM - 04:15 PM | Bolton Bailey and Xiaohong Chen (UIUC) | Verification in the RISC-Zero zkVM |
| 04:15 PM - 04:20 PM | Alley Stoughton (BU) | DSL for expressing UC designs in EasyUC |
| 04:20 PM - 04:25 PM | Mike Dodds (Galois) | Crypto verification and safe parsing |
| 04:25 PM - 04:55 PM | Break | |
| Databases | ||
| 04:55 PM - 05:15 PM | Yun-Sheng Chang (MIT) | Verifying a multi-version concurrency control database |
| 05:15 PM - 05:20 PM | Cheng Tan (NEU) | Verifying the Isolation levels of Databases Unilaterally |
| Rust verification | ||
| 05:20 PM - 05:40 PM | Andrea Lattuada (ETHZ) | Rust verification with Verus |
| 05:40 PM - 06:00 PM | Jonathan Protzenko (MSR) | Rust verification with Aeneas |
| Verification tooling | ||
| 06:00 PM - 06:05 PM | John Sarracino (Cornell) | MirrorSolve: Automating first-order Coq proofs using certified reflection and SMT |
| 06:05 PM - 06:10 PM | Sam Gruetter and Thomas Bourgeat (MIT) | E-Graphs to Help Writing Coq Proofs |
| 06:10 PM - 06:15 PM | Max Willsey (UW) | egglog: Combining E-Graphs and Datalog |
| Learning | ||
| 06:15 PM - 06:20 PM | Yue Meng (MIT) | Learning Density Distribution of Reachable States and Applications in Safe Autonomous Motion Planning |
| 06:20 PM | Adjourn -- dinner on your own (we can suggest good places to go) | |
For 20-minute talk slots: please give a 10-15 minute talk, leaving 5-10 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, and 2021.
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 September 15th.
Thanks to Google's OpenTitan team and NSF for providing the funding for the food at this workshop.
