| 10:00-11:30 | Registration | |
| 11:30-13:00 | Lunch | |
| Green Lounge | Attic Classroom | |
| 13:00-13:10 | Opening Ceremony | |
| 13:10-14:10 | Günther Raidl (Invited Talk, chair: Lukáš Sekanina) Combining Metaheuristics with Mathematical Programming Techniques for Solving Difficult Network Design Problems | |
| Formal Verification 1 Chair: Petr Jančar | Computer Systems 1 Chair: Günther Raidl | |
| 14:30-14:55 | Tomas Brazdil, Vaclav Brozek, Kousha Etessami, Antonin Kucera and Dominik Wojtczak One-Counter Markov Decision Processes | Zdenek Vasicek and Lukas Sekanina Efficient Hardware Accelerator for Symbolic Regression Problems |
| 14:55-15:20 | Tomas Brazdil, Vojtech Forejt, Jan Krcal, Jan Kretinsky and Antonin Kucera Continuous-Time Stochastic Games with Time-Bounded Reachability | Jakob Lechner and Marcus Jeitler Comparing the Robustness of Synchronous and Asynchronous Circuits by Fault Injection |
| 15:20-15:50 | Coffee Break | |
| Formal Verification 2 Chair: Petr Hliněný | Computer Systems 2 Chair: Hana Kubátová | |
| 15:50-16:15 | Kim G. Larsen, Uli Fahrenberg and Claus Thrane A Quantitative Characterization of Weighted Kripke Structures in Temporal Logic | Roland Dobai and Elena Gramatová Deductive Fault Simulation for Asynchronous Sequential Circuits |
| 16:15-16:40 | Lukas Holik and Jiri Simacek Optimizing an LTS-Simulation Algorithm | Martin Straka and Zdenek Kotasek Reliability Models for Fault Tolerant Architectures Based on FPGA |
| 16:40-17:00 | Frédéric Haziza Model-Checking Race-Freeness | Vaclav Simek and Radim Dvorak GPU Accelerated Solver of Time-Dependent Air Pollutant Transport Equations |
| 17:00-17:20 | Nikola Benes, Milan Krivanek and Filip Stefanak Space Effective Model Checking for Component-Interaction Automata | Jan Gaura, Eduard Sojka and Rostislav Dudek Surface Tension Measurement of Melted Metals and Slag by the Methods of Image Analysis |
| Formal Verification 3 Chair: Andrey Rybalchenko | Computer Security Chair: Vashek Matyáš | |
| 17:40-18:05 | Ahmed Bouajjani, Cezara Dragoi, Constantin Enea and Mihaela Sighireanu A Logic-based Framework for Reasoning about Composite Data | Martin Novotny COPACOBANA-Assisted Cryptoanalysis of GSM Communication |
| 18:05-18:30 | Nikola Benes, Lubos Brim, Ivana Cerna, Jiri Sochor, Pavlina Varekova and Barbora Buhnova Partial Order Reduction for State/Event LTL | Zbynek Michlovsky, Shaoning Pang and Nik Kasabov String Kernel Based SVM for Internet Security Implementation |
| 18:30-18:55 | Jiri Barnat, Lubos Brim, Milan Ceska and Tomas Lamr CUDA accelerated LTL Model Checking | Jiri Kur, Vashek Matyas and Petr Svenda Evolutionary design of attack strategies |
| 19:30 | Dinner, Wine Bar |