Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
svarm:program [2010/07/12 16:37] vkuncak |
svarm:program [2010/07/28 12:06] piskac |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Synthesis, Verification, and Analysis of Rich Models (SVARM 2010) ====== | ====== Synthesis, Verification, and Analysis of Rich Models (SVARM 2010) ====== | ||
+ | |||
+ | {{:svarm:program.pdf|Program in PDF Format}} | ||
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. | 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. | ||
Line 19: | Line 21: | ||
| 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 | | //Session Chair: Paul Jackson// | | | 14:00 | | //Session Chair: Paul Jackson// | | ||
- | | 14:00 | Natarajan Shankar | Inference Architectures for Satisfiability Modulo Theories | | + | | 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 | ||
Line 31: | Line 33: | ||
| | | | | | | | ||
| | | //Session Chair: Enric Rodríguez Carbonell// | | | | | //Session Chair: Enric Rodríguez Carbonell// | | ||
- | | 17:00 | Armin Biere and Florian Lonsing | Extending the BTOR Language | | + | | 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]] | | | 17:30 | Management Committee | [[mcagenda|Management Committee Meeting of Action IC0901]] | | ||
Line 52: | Line 54: | ||
| | | //Session Chair: Predrag Janicic// | | | | | //Session Chair: Predrag Janicic// | | ||
| 11:30 | Stefan Ratschan | Verification of Mixed Discrete-Continuous Systems | | | 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 | | + | | 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 | | + | | 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 | | //Session Chair: Maria Paola Bonacina// | | ||
Line 62: | Line 64: | ||
| 15:20 | | //Session Chair: Viktor Kuncak// | | | 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** ^ ^ | ||