Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
svarm:program [2010/07/08 11:46]
vkuncak
svarm:program [2010/09/06 00:02] (current)
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// ​
 +| 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]] | | 20:00 |  | [[http://​www.davidbann.com/​|Organized Dinner in David Bann vegetarian restaurant]] |
  
Line 31: Line 42:
  
 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 | Mariangiola Dezani-Ciancaglini,​ Silvia Ghilezan, Svetlana Jaksic and Jovanka Pantovic | Types for dynamic web data with RBAC  +| 15:20 |    | //Session Chair: Viktor Kuncak// | 
-| 15:40 | Predrag Janicic and Filip Maric | Uniform reduction to SMT  |+| 15:20 | Mariangiola Dezani-Ciancaglini,​ Silvia Ghilezan, Svetlana Jaksic and Jovanka Pantovic | Types for dynamic web data with RBAC   {{:​svarm:​jaksicSlides.pdf|slides}} ​
 +| 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** ^ ^