Program of SVARM

Tuesday, July 20th

Tuesday's program is also available with abstracts and side by side with other events.

09:00‑10:00 Session 1
Location: IF G.07
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:30‑12:30 Session 2
Location: IF G.07
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
14:00‑15:00 Invited Talk
Location: IF G.07
14:00 Natarajan Shankar
Inference Architectures for Satisfiability Modulo Theories
16:30‑18:00 Session 3
Location: IF G.07
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
Wednesday, July 21st

Wednesday's program is also available with abstracts and side by side with other events.

09:00‑10:00 Invited Talk
Location: IF G.07
09:00 Bernhard Beckert
Formal Verification of System Software
10:20‑11:20 Session 4
Location: IF G.07
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:30‑12:30 Session 5
Location: IF G.07
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
14:00‑15:00 Session 6
Location: IF G.07
14:00 Paul Jackson and Grant Passmore
Verification of Mixed Discrete-Continuous Systems
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:20‑16:20 Session 7
Location: IF G.07
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