This is an old revision of the document!
Synthesis, Verification, and Analysis of Rich Models (SVARM 2010)
Below is the program of SVARM, joint with PSY and a shared EMSQMS panel. SVARM is affiliated with CAV and IJCAR and is part of FLoC. It is supported by the COST Action Rich Model Toolkit. Please register here to participate.
Tuesday, July 20: Synthesis and Infrastructure
Location: Room 4.31+4.33 in IF building
| 08:50 | Paul Jackson | Welcome |
| 09:00 | Ras Bodik | Next Steps in Partial-Program Synthesis |
| 09:30 | Kim Larsen | Controller Synthesis from Timed Game Automata – from Theory to Practice |
| 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 | Tobias Nipkow | Automatic proof and disproof in Isabelle |
| 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:15 - | Discussion after the panel | |
| 17:00 | Armin Biere and Florian Lonsing | Extending the BTOR Language |
| 17:30 | Action IC0901 | Management Committee Meeting |
| 20:30 | (Tentative) Organized Dinner |
Wednesday, July 21: Verification and Automated Reasoning
Location: Room 4.31+4.33 in IF building
| 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 | Towards an Interpolating First-Order Prover |
| 16:20 | Closing Discussions |