Synthesis, Verification, and Analysis of Rich Models (SVARM 2010)
We are pleased to announce the program of SVARM 2010, joint with PSY and a shared EMSQMS panel. The program includes a number of invited talks as well as well as contributed presentations.
SVARM is affiliated with CAV and IJCAR and is part of FLoC. It is supported by the COST Action Rich Model Toolkit (http://richmodels.org)
Tuesday, July 20: Synthesis and Infrastructure
Location: Forum G.07 in IF building
| 08:50 | Paul Jackson | Welcome and Opening |
|---|---|---|
| 09:00 | Session Chair: Roderick Bloem | |
| 09:00 | Ras Bodik | Next Steps in Partial-Program Synthesis slides |
| 09:30 | Kim Larsen | Controller Synthesis from Timed Game Automata – from Theory to Practice |
| 10:00 - 10:30 | Coffee Break | |
| 10:30 | Session Chair: Cesar Sanchez | |
| 10:30 | Alexander Rabinovich | Extensions of the Church synthesis Problem |
| 11:00 | Bernd Finkbeiner | Coordination Logic |
| 11:30 | Georg Hofferek and Roderick Bloem | Controller Synthesis Using Uninterpreted Functions slides |
| 12:00 | Tobias Nipkow | Automatic proof and disproof in Isabelle slides |
| 12:30 - 14:00 | LUNCH | |
| 14:00 | Session Chair: Paul Jackson | |
| 14:00 | Natarajan Shankar | Inference Architectures for Satisfiability Modulo Theories slides |
| 15:00 - 15:30 | Coffee Break | |
| 15:30 - 16:15 | Panel joint with Evaluation Methods for Solvers and Quality Metrics for Solutions | |
| 16:15 - | Discussion on Quality Metrics for Solutions | |
| Session Chair: Enric Rodríguez Carbonell | ||
| 17:00 | Armin Biere and Florian Lonsing | Extending the BTOR Language slides |
| 17:30 | Management Committee | Management Committee Meeting of Action IC0901 |
| 20:00 | Organized Dinner in David Bann vegetarian restaurant |
Wednesday, July 21: Verification and Automated Reasoning
Location: Forum G.07 in IF building
| 09:00 | Session Chair: Tobias Nipkow | |
| 09:00 | Bernhard Beckert | Formal Verification of System Software slides |
| 10:00 - 10:20 | Coffee Break | |
|---|---|---|
| 10:20 | Session Chair: Tayssir Touili | |
| 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 slides |
| 11:20 | Mini Break of 10 minutes | |
| Session Chair: Predrag Janicic | ||
| 11:30 | Stefan Ratschan | Verification of Mixed Discrete-Continuous Systems slides |
| 11:50 | Alejandro Sanchez and Cesar Sanchez | Towards Temporal Verification of Concurrent Data-structures: In Need for Sophisticated Decision Procedures slides |
| 12:10 | Hossein Hojjat, Viktor Kuncak, Ruzica Piskac and Philippe Suter | Vepar: A Framework for Automated Reasoning slides |
| 12:30 - 14:00 | LUNCH | |
| 14:00 | Session Chair: Maria Paola Bonacina | |
| 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 | Session Chair: Viktor Kuncak | |
| 15:20 | Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jaksic and Jovanka Pantovic | Types for dynamic web data with RBAC slides |
| 15:40 | Predrag Janicic and Filip Maric | Uniform reduction to SMT slides |
| 16:00 | Maria Paola Bonacina and Moa Johansson | Towards an Interpolating First-Order Prover |
| 16:20 | Closing Discussions |