====== Synthesis, Verification, and Analysis of Rich Models (SVARM 2010) ======

**Preliminary Program of [[:SVARM]]**

===== Day 1: Synthesis and Infrastructure =====

09:00 [[http://research.ihost.com/psy2010/|(PSY)]] Ras Bodik

09:30 [[http://research.ihost.com/psy2010/|(PSY)]] Kim Larsen

10:00 - 10:30 **Coffee Break**

10:30 Alexander Rabinovich: Extensions of the Church synthesis Problem

11:00 [[http://research.ihost.com/psy2010/|(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 [[http://clc.cs.uiowa.edu/EMSQMS/|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

===== Day 2: Verification and Automated Reasoning =====

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**