Preliminary Program of SVARM
09:00 (PSY) Ras Bodik
09:30 (PSY) Kim Larsen
10:00 - 10:30 Coffee Break
10:30 Alexander Rabinovich: Extensions of the Church synthesis Problem
11:00 (PSY) Bernd Finkbeiner: Bounded Synthesis
11:30 Georg Hofferek and Roderick Bloem: Controller Synthesis Using Uninterpreted Functions
12:00 Barbara Jobstmann: Quantitative Verification and Synthesis
12:30 - 14:00 LUNCH
14:00 Invited Talk: Natarajan Shankar: Inference Architectures for Satisfiability Modulo Theories
15:00 - 15:30 Coffee Break
15:30 - 16:15 Panel joint with Evaluation Methods for Solvers and Quality Metrics for Solutions
16:30 Armin Biere and Florian Lonsing. Extending the BTOR Language
17:00 Tobias Nipkow: Automatic proof and disproof in Isabelle
17:30 MC Meeting
09:00 Invited Talk: Bernhard Beckert: Formal Verification of System Software
10:00 - 10:20 Coffee Break
10:20 Peter Schneider-Kamp. Towards Complexity and Termination Analysis of Transition Systems
10:40 Peter Habermehl, Lukas Holik, Adam Rogalewicz, Jiri Simacek and Tomas Vojnar. A Proposal of a New Automata-based Representation of Heaps
11:00 Marius Bozga, Radu Iosif, Filip Konecny and Tomas Vojnar. FLATA: Towards a Toolset for manipulation and analysis of counter automata
11:20 Mini Break of 10 minutes
11:30 Stefan Ratschan. Verification of Mixed Discrete-Continuous Systems
11:50 Alejandro Sanchez and Cesar Sanchez. Towards Temporal Verification of Concurrent Data-structures: In Need for Sophisticated Decision Procedures
12:10 Hossein Hojjat, Viktor Kuncak, Ruzica Piskac and Philippe Suter. Vepar: A Framework for Automated Reasoning
12:30 - 14:00 LUNCH
14:00 Paul Jackson and Grant Passmore. Applications of a procedure for solving non-linear arithmetic problems
14:20 Cristina Borralleras, Salvador Lucas, Albert Oliveras, Enric RodrÃguez Carbonell and Albert Rubio. Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic
14:40 Timothy Nelson, Dougherty Daniel, Kathi Fisler and Shriram Krishnamurthi: On the Finite Model Property in Order-Sorted Logic
15:00 - 15:20 Coffee Break
15:20 Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic and Jovanka Pantovic: Types for dynamic web data with RBAC
15:40 Predrag Janicic and Filip Maric. Uniform reduction to SMT
16:00 Maria Paola Bonacina and Moa Johansson. Advances in rewrite-based decision procedures
16:20 Closing Discussions