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

Program in PDF Format

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 (

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