The 2017 New England Systems Verification Day will take place on Friday, October 6th, 2017, in room 32-G449 ("Kiva") at the Stata Center (32 Vassar St, Cambridge, MA 02139).
For any attendees that are around on Thursday, October 5th, 2017 (the day before the workshop), we will organize a dinner in the evening.
| Time | Speaker | Topic |
|---|---|---|
| Long talks on larger projects | ||
| 8:30am | Luke Nelson, Helgi Sigurbjarnarson, Xi Wang (U. Washington) | [LONG] Push-button verification |
| 9:30am | Bryan Parno, Chris Hawblitzel, et al. (Microsoft Research) | [LONG] Everest |
| 10:30am | BREAK | |
| Medium-length talks on hardware verification | ||
| 11:00am | Pramod Subramanyan et al. (UC Berkeley and MIT) | [MEDIUM] Specification and verification of trusted platforms |
| 11:20am | Andrew Myers (Cornell) | [MEDIUM] Hardware information flow |
| 11:40am | Murali Vijayaraghavan (MIT) | [MEDIUM] Verified Bluespec designs |
| Noon | Lunch | |
| Long talks on larger projects | ||
| 1:30pm | Andres Erbsen, Jade Philipoom, Jason Gross (MIT) | [LONG] Verified elliptic curve crypto |
| 2:30pm | Zhong Shao, Ronghui Gu, et al. (Yale) | [LONG] CertiKOS |
| 3:30pm | BREAK | |
| Medium-length talks unrelated to hardware verification | ||
| 4:00pm | Jay Lorch et al. (Microsoft Research) | [MEDIUM] Verifying concurrent programs |
| 4:20pm | Benjamin Delaware et al. (Purdue and MIT) | [MEDIUM] Fiat |
| 4:40pm | Tej Chajed et al. (MIT) | [MEDIUM] FSCQ |
| Short talks on problems for verification | ||
| 5:00pm | Nick Mathewson (Tor) | [SHORT] Tor |
| 5:05pm | Chris Casinghino (Draper) | [SHORT] Extracting good specifications from engineers |
| 5:10pm | Benjamin Kaiser (Lincoln) | [SHORT] Formally verified software updates for aircraft and satellites |
| 5:15pm | Jon McCune (Google) | [SHORT] Security root-of-trust chip |
| 5:20pm | Jon Howell (Google) | [SHORT] Using Verification in Anger |
| Short talks on other verification projects | ||
| 5:25pm | Daniel Schwartz-Narbonne (Amazon) | [SHORT] Timing side channels for crypto code |
| 5:30pm | Greg Morrisett (Cornell) | [SHORT] CertiCoq |
| 5:35pm | Alley Stoughton, Mayank Varia (Boston U.) | [SHORT] EasyCrypt meets UC |
| 5:40pm | Carsten Varming (Amazon) | [SHORT+] Checking equivalence of access-management policies |
| 5:50pm | BREAK | |
| 6:00pm | Reception / dinner | |
