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