Schedule
Wednesday 15 | |
| 14:00 - 15:00 | Sanjit Seshia |
| Solvers, Abstraction, and Inductive Learning
slides
| |
| 15:30 - 16:30 | Ashish Tiwari |
| Programming with Primal and Dual Semantics | |
Thursday 16 | |
| 9:00 - 10:00 | Sandrine Blazy |
| Towards a formally verified obfuscating compiler
slides
| |
| 10:30 - 11:30 | Klaus Havelund |
| K: a wide spectrum textual language for modeling and
implementation
slides
| |
| 13:00 - 14:00 | Nirav Dave |
| Verifying a RISC-V Processor | |
Prashanth Mundkur |
|
| Specifying the RISC-V ISA
| |
| 15:00 - 16:00 | Jean-Christophe Filliātre |
| Computing the Littlewood-Richardson coefficients
slides
| |
| 16:00 - 17:00 | Jim Woodcock |
| Discussion on FreeRTOS:
Refinement, Concurrency, and Simulation
| |
Friday 17 | |
| 9:00 - 10:30 | Ernie Cohen |
| Weak Memory Models
| |
| 11:00 - 12:00 | Gary Leavens |
| Citizen Computer Science
| |
| 13:00 - 14:00 | Wolfgang Paul |
| Theoretical lectures on practical system architecture
| |
| 14:00 - 15:00 | Sylvain Conchon |
| Cubicle: Certifying the results of an SMT-based model
checker for parameterized systems
|
Participants
- Sandrine Blazy
- Ernie Cohen
- Sylvain Conchon (invited observer)
- Jean-Christophe Filliātre
- Klaus Havelund
- Gary Leavens (chair)
- Prashanth Mundkur (invited observer)
- Wolfgang Paul
- Sanjit Seshia (invited observer)
- Natarajan Shankar (secretary, host)
- Ashish Tiwari (invited observer)
- Jim Woodcock
Last updated: July 15, 2015