Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
svarm:program [2010/07/07 23:50] vkuncak |
svarm:program [2010/08/20 12:39] piskac |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Synthesis, Verification, and Analysis of Rich Models (SVARM 2010) ====== | ====== Synthesis, Verification, and Analysis of Rich Models (SVARM 2010) ====== | ||
| - | We are pleased to announce the program of [[:SVARM]], joint with [[http://research.ihost.com/psy2010/|PSY]] and a shared [[http://clc.cs.uiowa.edu/EMSQMS/|EMSQMS panel]]. The program includes a number of invited talks as well as well as contributed presentations. | + | {{:svarm:program.pdf|Program in PDF Format}} |
| - | SVARM is affiliated with [[http://www.floc-conference.org/CAV-home.htm|CAV]] and [[http://www.floc-conference.org/IJCAR-home.html|IJCAR]] and is part of [[http://www.floc-conference.org/|FLoC]]. It is supported by the [[http://www.cost.eu|COST]] Action [[:|Rich Model Toolkit]]. Please [[http://www.floc-conference.org/registration.html|register here]] to participate. | + | We are pleased to announce the program of **SVARM 2010**, joint with [[http://research.ihost.com/psy2010/|PSY]] and a shared [[http://clc.cs.uiowa.edu/EMSQMS/|EMSQMS panel]]. The program includes a number of invited talks as well as well as contributed presentations. |
| + | |||
| + | SVARM is affiliated with [[http://www.floc-conference.org/CAV-home.htm|CAV]] and [[http://www.floc-conference.org/IJCAR-home.html|IJCAR]] and is part of [[http://www.floc-conference.org/|FLoC]]. It is supported by the [[http://www.cost.eu|COST]] Action [[:|Rich Model Toolkit]] (http://richmodels.org) | ||
| ====== Tuesday, July 20: Synthesis and Infrastructure ====== | ====== Tuesday, July 20: Synthesis and Infrastructure ====== | ||
| - | Location: [[http://www.floc-conference.org/location.html | + | Location: [[http://www.floc-conference.org/location.html|Forum G.07 in IF building]] |
| - | |Room 4.31+4.33 in IF building]] | + | |
| ^ 08:50 ^ Paul Jackson ^ Welcome and Opening ^ | ^ 08:50 ^ Paul Jackson ^ Welcome and Opening ^ | ||
| - | | 09:00 | Ras Bodik | Next Steps in Partial-Program Synthesis | | + | | | | |
| + | | 09:00 | | //Session Chair: Roderick Bloem// | | ||
| + | | 09:00 | Ras Bodik | Next Steps in Partial-Program Synthesis {{:svarm:bodikSlides.ppt|slides}} | | ||
| | 09:30 | Kim Larsen | Controller Synthesis from Timed Game Automata -- from Theory to Practice | | | 09:30 | Kim Larsen | Controller Synthesis from Timed Game Automata -- from Theory to Practice | | ||
| ^ 10:00 - 10:30 ^ **Coffee Break** ^ ^ | ^ 10:00 - 10:30 ^ **Coffee Break** ^ ^ | ||
| + | | | | | ||
| + | | 10:30 | | //Session Chair: Cesar Sanchez// | | ||
| | 10:30 | Alexander Rabinovich | Extensions of the Church synthesis Problem | | | 10:30 | Alexander Rabinovich | Extensions of the Church synthesis Problem | | ||
| | 11:00 | Bernd Finkbeiner | Coordination Logic | | | 11:00 | Bernd Finkbeiner | Coordination Logic | | ||
| - | | 11:30 | Georg Hofferek and Roderick Bloem | Controller Synthesis Using Uninterpreted Functions | | + | | 11:30 | Georg Hofferek and Roderick Bloem | Controller Synthesis Using Uninterpreted Functions {{:svarm:hofferekSlides.pdf|slides}} | |
| - | | 12:00 | Tobias Nipkow | Automatic proof and disproof in Isabelle | | + | | 12:00 | Tobias Nipkow | Automatic proof and disproof in Isabelle {{:svarm:nipkowSlides.pdf|slides}} | |
| ^ 12:30 - 14:00 ^ **LUNCH** ^ ^ | ^ 12:30 - 14:00 ^ **LUNCH** ^ ^ | ||
| - | | 14:00 | Natarajan Shankar | Inference Architectures for Satisfiability Modulo Theories | | + | | | | |
| + | | 14:00 | | //Session Chair: Paul Jackson// | | ||
| + | | 14:00 | Natarajan Shankar | Inference Architectures for Satisfiability Modulo Theories {{:svarm:shankarslides.pdf|slides}} | | ||
| ^ 15:00 - 15:30 ^ **Coffee Break** ^ ^ | ^ 15:00 - 15:30 ^ **Coffee Break** ^ ^ | ||
| | 15:30 - 16:15 | | [[http://clc.cs.uiowa.edu/EMSQMS/|Panel joint with Evaluation Methods for Solvers and | | 15:30 - 16:15 | | [[http://clc.cs.uiowa.edu/EMSQMS/|Panel joint with Evaluation Methods for Solvers and | ||
| Quality Metrics for Solutions]] | | Quality Metrics for Solutions]] | | ||
| - | | 16:15 - | | Discussion after the panel | | + | | 16:15 - | | Discussion on Quality Metrics for Solutions | |
| - | | 17:00 | Armin Biere and Florian Lonsing | Extending the BTOR Language | | + | | | | |
| - | | 17:30 | Action IC0901 | Management Committee Meeting | | + | | | | //Session Chair: Enric Rodríguez Carbonell// | |
| - | | 20:00+ | | [[http://www.davidbann.com/|Organized Dinner in David Bann vegetarian restaurant]] | | + | | 17:00 | Armin Biere and Florian Lonsing | Extending the BTOR Language {{:svarm:biereSlides.pdf|slides}} | |
| + | | | | | ||
| + | | 17:30 | Management Committee | [[mcagenda|Management Committee Meeting of Action IC0901]] | | ||
| + | | | | | ||
| + | | 20:00 | | [[http://www.davidbann.com/|Organized Dinner in David Bann vegetarian restaurant]] | | ||
| ====== Wednesday, July 21: Verification and Automated Reasoning ====== | ====== Wednesday, July 21: Verification and Automated Reasoning ====== | ||
| Location: [[http://www.floc-conference.org/location.html | Location: [[http://www.floc-conference.org/location.html | ||
| - | |Room 4.31+4.33 in IF building]] | + | |Forum G.07 in IF building]] |
| - | | 09:00 | Bernhard Beckert | Formal Verification of System Software | | + | | 09:00 | | //Session Chair: Tobias Nipkow// | |
| + | | 09:00 | Bernhard Beckert | Formal Verification of System Software {{:svarm:beckertSlides.pdf|slides}} | | ||
| ^ 10:00 - 10:20 ^ **Coffee Break** ^ ^ | ^ 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: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 | | | 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:00 | Marius Bozga, Radu Iosif, Filip Konecny and Tomas Vojnar | FLATA: Towards a Toolset for manipulation and analysis of counter automata {{:svarm:konecnySlides.pdf|slides}} | |
| ^ 11:20 ^ **Mini Break of 10 minutes** ^ ^ | ^ 11:20 ^ **Mini Break of 10 minutes** ^ ^ | ||
| - | | 11:30 | Stefan Ratschan | Verification of Mixed Discrete-Continuous Systems | | + | | | | //Session Chair: Predrag Janicic// | |
| - | | 11:50 | Alejandro Sanchez and Cesar Sanchez | Towards Temporal Verification of Concurrent Data-structures: In Need for Sophisticated Decision Procedures | | + | | 11:30 | Stefan Ratschan | Verification of Mixed Discrete-Continuous Systems {{:svarm:ratschanSlides.pdf|slides}} | |
| - | | 12:10 | Hossein Hojjat, Viktor Kuncak, Ruzica Piskac and Philippe Suter | Vepar: A Framework for Automated Reasoning | | + | | 11:50 | Alejandro Sanchez and Cesar Sanchez | Towards Temporal Verification of Concurrent Data-structures: In Need for Sophisticated Decision Procedures {{:svarm:sanchezSlides.pdf|slides}} | |
| + | | 12:10 | Hossein Hojjat, Viktor Kuncak, Ruzica Piskac and Philippe Suter | Vepar: A Framework for Automated Reasoning {{:svarm:hojjatSlides.pdf|slides}} | | ||
| ^ 12:30 - 14:00 ^ **LUNCH** ^ ^ | ^ 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: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: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 | | | 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: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 | | | 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 | | + | | 15:40 | Predrag Janicic and Filip Maric | Uniform reduction to SMT {{:svarm:janicicSlides.pdf|slides}} | |
| | 16:00 | Maria Paola Bonacina and Moa Johansson | Towards an Interpolating First-Order Prover | | | 16:00 | Maria Paola Bonacina and Moa Johansson | Towards an Interpolating First-Order Prover | | ||
| ^ 16:20 ^ **Closing Discussions** ^ ^ | ^ 16:20 ^ **Closing Discussions** ^ ^ | ||