Time | | |
| | |
09:00-10:00 | | Invited Talk
Chair: Bob R. Kurshan |
| |
David M. Rusinoff
A Mathematical Approach to RTL Verification
|
| | |
10:00-10:30 | | Coffee Break |
| | |
10:30-12:15 | | Session IV: Shapes
Session Chair: Holger Hermanns |
|
10:30-11:00
|
Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter O'Hearn, Thomas Wies and Hongseok Yang
Shape Analysis for Composite Data Structures
|
| | |
| 11:00-11:30 | Ranjit Jhala and Ken McMillan
Array Abstractions from Proofs |
| | |
| 11:30-12:00 | Ahmed Bouajjani, Severine Fratani and Shaz Qadeer
Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures |
| | |
| 12:00-12:15 | Igor Bogudlov, Tal Lev-Ami, Thomas Reps and Mooly Sagiv
Revamping TVLA: Making Parametric Shape Analysis Competitive |
| | |
12:15-13:45 | | Lunch Break |
| | |
13:45-15:00 | | Session VII: Concurrent Program Verification
Session Chair: Armin Biere |
|
13:45-14:15
|
Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan and Aarti Gupta
Fast and Accurate Static Data Race Detection for Concurrent Programs
|
| | |
| 14:15-14:45 | Feng Chen and Grigore Rosu
Parametric and Sliced Causality |
| | |
| 14:45-15:00 | Gael Patin, Mihaela Sighireanu and Tayssir Touili
SPADE: Verification of Multithreaded Dynamic and Recursive Programs |
| | |
15:00-15:30 | | Session VIII: Reactive Designs
Session Chair: Parosh Abdullah |
|
15:00-15:15
|
Barbara Jobstmann, Stefan Galler, Martin Weiglhofer and Roderick Bloem
Anzu: A Tool for Property Synthesis
|
| | |
| 15:15-15:30 | Roderick Bloem, Roberto Cavada, Ingo Pill, Marco Roveri and Andrei Tchaltsev
RAT: A Tool for the Formal Analysis of Requirements |
| | |
15:30-16:00 | | Coffee Break |
| | |
17:00-open | | Excursion / Banquet
The Excursion will be a boat tour to 'Insel Lindwerder'
Meeting Point:
Burgstraße/Bodestraße
|
