Time | | |
| | |
09:00-10:00 | | Invited Talk
Chair: Werner Damm |
| |
Thomas Kropf
Software Bugs seen from an Industrial Perspective
or
Can Formal Methods help on Automotive Software Development?
|
| | |
10:00-10:30 | | Coffee Break |
| | |
10:30-11:30 | | Session IX: Parallelisation
Session Chair: Werner Damm |
|
10:30-11:00
|
Jonathan Ezekiel, Gerald Lüttgen and Gianfranco Ciardo
Parallelising Symbolic State-Space Generators
|
| | |
| 11:00-11:30 | Jiri Barnat, Lubos Brim and Pavel Simecek
I/O Efficient Accepting Cycle Detection |
| | |
11:30-12:30 | | Session X: Constraints and Decisions
Session Chair: Alessandro Cimatti |
|
11:30-11:45
|
Robert Brummayer and Armin Biere
C32SAT: Checking C Expressions
|
| | |
| 11:45-12:00 | Clark Barrett and Cesare Tinelli
CVC3 |
| | |
| 12:00-12:15 | Panagiotis Manolios, Daron Vroon and Sudarshan Srinivasan
BAT: The Bit-Level Analysis Tool |
| | |
| 12:15-12:30 | Bernd Becker, Christian Dax, Jochen Eisinger and Felix Klaedtke
LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals |
| | |
12:30-14:00 | | Lunch Break |
| | |
14:00-15:30 | | Session XI: Probabilistic Verification
Session Chair: Holger Hermanns |
|
14:00-14:30
|
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, and Verena Wolf
Three-Valued Abstraction for Continuous-Time Markov Chains
|
| | |
| 14:30-15:00 | Pritam Roy and Luca de Alfaro
Magnifying-Lens Abstraction for Markov Decision Processes |
| | |
| 15:00-15:30 | Ofer Strichman and Arie Matsliah
Underapproximation for Model-Checking Based on Random Cryptographic Constructions |
| | |
15:30-16:00 | | Coffee Break |
| | |
16:00-18:00 | | Session XII: Abstraction
Chair: Ahmed Bouajjani |
|
16:00-16:30
|
Chao Wang, Zijiang Yang, Aarti Gupta and Franjo Ivancic
Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra
|
| | |
| 16:30-17:00 | Domagoj Babic and Alan Hu
Structural Abstraction of Software Verification Conditions |
| | |
| 17:00-17:30 | Sumit Gulwani and Ashish Tiwari
An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software |
| | |
| 17:30-18:00 | Thomas Wahl
Adaptive Symmetry Reduction |
| | |
18:00-19:00 | | Business Meeting |
| | |
20:00-open | | SC-Dinner (SC-Members and Chairs only) |
