The 2019 New England Systems Verification Day will take place on Friday, October 18th, 2019, in room 32-G449 ("Kiva") at the Stata Center (32 Vassar St, Cambridge, MA 02139).
| Time | Speaker | Topic |
|---|---|---|
| 8:00am | Breakfast available | |
| 9:00am | Jon Howell (VMware Research) | VeriBetrFS: verified filesystem using Iron* methodology |
| 9:20am | Mo Zou (Shanghai Jiao Tong) | AtomFS: verifying a concurrent file system with helpers |
| 9:40am | Ronghui Gu (Columbia) | Linux KVM micro-verification |
| 10:00am | Gregory Malecha (BedRock Systems) | Verification on top of a Capability Based Microkernel |
| 10:20am | BREAK | |
| 10:50am | Joshua Gancher (Cornell) | IPDL: proving compositional security of cryptographic protocols |
| 11:10am | Bryan Parno (CMU) | Project Everest update |
| 11:25am | Tim Braje (Lincoln Lab) | Formal Verification of Design Patterns for Cryptographic Protocols |
| 11:40am | Alley Stoughton (Boston U.) | UC security in EasyCrypt |
| 11:45am | Anish Athalye (MIT) | Notary: device for secure transaction approval |
| Noon | Lunch | |
| 1:00pm | Drew Zagieboylo (Cornell) | Information-flow contract for secure processors |
| 1:20pm | Murali Vijayaraghavan (SiFive) | Building RISC-V processors using Coq at SiFive |
| 1:35pm | Clement Pit-Claudel, Thomas Bourgeat (MIT) | Verified compiler for a Bluespec-style hardware language |
| 1:50pm | Rajit Manohar (Yale) | Integrated verification and synthesis for asynchronous logic |
| 2:05pm | Steve Crocker | IMP: a verification challenge |
| 2:10pm | BREAK | |
| 2:40pm | Luke Nelson (U. Washington) | Serval: automated verification of systems code |
| 3:00pm | Andres Erbsen (MIT) | Hardware/software verification for IoT |
| 3:15pm | Chris Casinghino (Draper) | Policy language for tagged architecture |
| 3:30pm | Sam Lasser (Tufts) | Verified LL(1) parser generator |
| 3:45pm | BREAK | |
| 4:15pm | Jay Lorch (Microsoft) | Verification of multi-threaded systems |
| 4:35pm | Tej Chajed (MIT) | Perennial: concurrent crash-safe systems |
| 4:50pm | Robert Armstrong (Sandia) | Dishwashers of Armageddon: Verifying high consequence systems for Nuclear Weapons |
| 5:10pm | Joe Tassarotti (Boston College), Jean-Baptiste Tristan (Oracle) | Formal verification for ML |
| 5:20pm | Paul Rowe (MITRE) | Attestation evidence in the presence of an adversary |
| 5:30pm | Reception / dinner |
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 and 2018.
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 1st.
