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 | ||
madrid13 [2013/09/13 16:25] cesar.sanchez |
madrid13 [2013/10/07 16:08] cesar.sanchez |
||
---|---|---|---|
Line 2: | Line 2: | ||
The workshop will be held at the IMDEA Software Institute in Madrid. There will be arrangements including transportation from a centric location near a hotel and special rates at the hotel. More information can be found in the Local Arrangements section. | The workshop will be held at the IMDEA Software Institute in Madrid. There will be arrangements including transportation from a centric location near a hotel and special rates at the hotel. More information can be found in the Local Arrangements section. | ||
+ | |||
+ | ===== PROGRAMME ===== | ||
+ | |||
+ | === Thursday, Oct 17 === | ||
+ | |||
+ | ^ ^ Speaker ^ Title ^ | ||
+ | | 9:00-10:00 | Invited Talk : Cesare Tinelli |Solving quantified formulas in SMT by finite model finding | | ||
+ | | 10:00 - 10:30 | ** Coffee break ** || | ||
+ | ^ SESSION 1 ^ SAT and SMT + Applications (Chair: Maria Paola Bonacina) ^^ | ||
+ | | 10:30 - 11:00 | Eivind Jahren | Maintenance Scheduling in the Oil Industry Using SMT Techniques | | ||
+ | | 11:00 - 11:30 | Predrag Janicic | Proving Correctness of a KRK Chess Endgame Strategy by SAT-Based Constraint Solving | | ||
+ | | 11:30 - 12:00 | Grant Passmore | Exact Global Nonlinear Optimization on Demand | | ||
+ | | 12:00 - 14:00 | ** Lunch ** || | ||
+ | ^ SESSION 2 ^ Formal Methods, Verification and Model Checking (Chair: Radu Iosif) ^^ | ||
+ | | 14:00 - 15:00 | Invited talk : Virginie Wiels | Formal Methods in Aerospace: Constraints, Assets and Challenges | | ||
+ | | 15:00 - 15:30 | Antti Hyvärinen | Verification-Aided Regression Testing | | ||
+ | | 15:30 - 16:00 | Pavle Subotic | Exploring Interpolants | | ||
+ | | 16:00 - 16:30 | ** Coffee Break ** || | ||
+ | ^ SESSION 3 ^ Synthesis and Games (Chair: Cesar Sanchez) ^^ | ||
+ | | 16:30 - 17:00 | Tihaomir Gvero | Synthesizing and Repairing Expressions using Types and Weights | | ||
+ | | 17:00 - 17:30 | Robert Koenighofer | QBF-Based Synthesis Methods for Safety Specifications | | ||
+ | | 17:30 - 18:00 | Guillermo Perez | Mean-payoff games: imperfect vs. incomplete information | | ||
+ | |||
+ | |||
+ | === Thursday, Oct 18 === | ||
+ | |||
+ | ^ ^ Title ^ Speaker ^ | ||
+ | ^ SESSION 4 ^ Program Verification and Reliability (Chair: Enric Rodriguez-Carbonell) ^^ | ||
+ | | 9:00-10:00 | Invited Talk : Willem Visser | Model Counting >= Symbolic Execution | | ||
+ | | 10:00 - 10:30 | ** Coffee break ** || | ||
+ | | 10:30 - 11:00 | Radu Iosif | Safety Problems are NP-complete for Flat Integer Programs with Octagonal Loops | | ||
+ | | 11:00 - 11:30 | Hossein Hojjat | Relational Invariants for Verification of Parameterized Timed Systems | | ||
+ | | 11:30 - 12:00 | Dana Drachsler | A Verification-Friendly Concurrent Binary Tree | | ||
+ | ^ 12:00 - 14:00 ^ ** BUSINESS MEETING / LUNCH ** ^^ | ||
+ | ^ SESSION 5 ^ Logics, Formal Languages and Semantics (Chair: Predrag Janicic) ^^ | ||
+ | | 14:00 - 14:30 | Tarmo Uustalu | A Hoare Logic for Reasoning About Nonterminating Behaviors | | ||
+ | | 14:30 - 15:00 | Denis Firsov | Formalizing Attribute Grammars and Circularity Checking | | ||
+ | | 15:00 - 15:30 | Adam Rogalewicz | The Tree Width of Separation Logic with Recursive Definitions | | ||
+ | | 15:30 - 16:00 | Gabriel Istrate |From simple combinatorial statements with difficult mathematical proofs to hard instances of SAT | | ||
+ | | 16:00 | Closing Remarks || | ||
+ | |||
+ | |||
===== Local Arrangements ===== | ===== Local Arrangements ===== | ||
Line 12: | Line 54: | ||
The Local Orgranization will reserve a private bus that will depart in the morning from the corner between Plaza Santo Domingo and Calle Jacometrezo ([[http://goo.gl/maps/4EptA|here]]). The bus will depart in the morning and return in the afternoon after the meeting finishes. This is a very centric area with plenty of accommodation options. IMDEA Software has reserved rooms at special prices (90 EUR + VAT) at the following hotels: | The Local Orgranization will reserve a private bus that will depart in the morning from the corner between Plaza Santo Domingo and Calle Jacometrezo ([[http://goo.gl/maps/4EptA|here]]). The bus will depart in the morning and return in the afternoon after the meeting finishes. This is a very centric area with plenty of accommodation options. IMDEA Software has reserved rooms at special prices (90 EUR + VAT) at the following hotels: | ||
- | [[http://www.hotelopera.com/|Hotel Opera]] | + | * [[http://www.hotelopera.com/|Hotel Opera]] |
+ | * [[http://www.hotelmeninas.es/|Hotel Meninas]] | ||
+ | |||
+ | Please use the code "COST" when making a reservation. To obtain the reduced price you need to contact : info@hotelopera.com . | ||
+ | **Social Event** | ||
+ | |||
+ | On the evening of Thu, 17, there will be an organized visit to the [[http://www.museoreinasofia.es/en|Museo Reina Sofia]], the museum of modern art in Madrid (the permanent collection includes Picasso's Guernica and many Dali's and Miro's). This visit will be covered by the local organizers. | ||
+ | |||
**Workshop Dinner** | **Workshop Dinner** | ||
- | To be announced | + | After the visit to the museum, there will be a workshop dinner. Dinner will not be covered by the local organizers. |
+ | The restaurant will be [[http://www.restaurantesamarkanda.com/|Samarkanda]], and the price will be roughly 40 EUR per person. | ||
+ | |||
+ | **Workshop Lunches** | ||
+ | |||
+ | Lunch will be served in the building next to IMDEA Software. The cost of lunch is 6 EUR per person. | ||
**Local Organisation Matters** | **Local Organisation Matters** | ||
If you have any questions regarding logistics you can email directly Cesar Sanchez([[cesar.sanchez@imdea.org]]) or Tania Rodriguez ([[tania.rodriguez@imdea.org]]). | If you have any questions regarding logistics you can email directly Cesar Sanchez([[cesar.sanchez@imdea.org]]) or Tania Rodriguez ([[tania.rodriguez@imdea.org]]). |