This is an old revision of the document!

====== Synthesis, Verification, and Analysis of Rich Models (SVARM 2010) ====== **Preliminary Program of [[:SVARM]]** joint with [[http://research.ihost.com/psy2010/|PSY]] and a shared [[http://clc.cs.uiowa.edu/EMSQMS/|SMSQMS panel]]. ===== Day 1: Synthesis and Infrastructure ===== | 09:00 | Ras Bodik | | | 09:30 | Kim Larsen | | ^ 10:00 - 10:30 ^ **Coffee Break** ^ ^ | 10:30 | Alexander Rabinovich | Extensions of the Church synthesis Problem | | 11:00 | 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 | Action IC0901 | Management Committee 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** ^ ^