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

Preliminary Program of SVARM

09:00 (PSY) Ras Bodik

09:30 (PSY) Kim Larsen

10:00 - 10:30 Coffee Break

10:30 Alexander Rabinovich: Extensions of the Church synthesis Problem

11:00 (PSY) 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 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 MC Meeting

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