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.