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
Next revision Both sides next revision
madrid13 [2013/09/13 16:25]
cesar.sanchez
madrid13 [2013/10/25 08:01]
enric.rodriguez.carbonell
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. ​
 +
 +===== NEWS (Transportation) =====
 +
 +The Local Orgranization will reserve a private bus that will depart at 8:15am in the morning from the corner between Plaza Santo Domingo and Calle Jacometrezo ([[http://​goo.gl/​maps/​4EptA|here]]). It will depart from IMDEA Software back to Madrid after the afternoon sessions.
 +
 +===== PROGRAMME =====
 +
 +=== Thursday, Oct 17 ===
 +
 +^             ^ Speaker ​                ^ Title ^
 +| 9:00-10:00 | Invited Talk : Cesare Tinelli | {{:​madrid13-slides-Cesare-Tinelli.pdf|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 | {{:​madrid13-slides-Eivind-Jahren.pdf|Maintenance Scheduling in the Oil Industry Using SMT Techniques}} |
 +| 11:00 - 11:30 | Predrag Janicic | {{:​madrid13-slides-Predrag-Janicic.pdf|Proving Correctness of a KRK Chess Endgame Strategy by SAT-Based Constraint Solving}} |
 +| 11:30 - 12:00 | Grant Passmore | {{:​madrid13-slides-Grant-Passmore.pdf|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 | {{:​madrid13-slides-Virginie-Wiels.pdf|Formal Methods in Aerospace: Constraints,​ Assets and Challenges}} |
 +| 15:00 - 15:30 | Antti Hyvärinen | {{:​madrid13-slides-Antti-Hyvärinen.pdf|Verification-Aided Regression Testing}} |
 +| 15:30 - 16:00 | Pavle Subotic | {{:​madrid13-abs-Pavle-Subotic.pdf|Exploring Interpolants}} |
 +| 16:00 - 16:30 | ** Coffee Break ** ||
 +^  SESSION 3 ^ Synthesis and Games (Chair: Cesar Sanchez) ^^
 +| 16:30 - 17:00 | Tihomir Gvero | {{:​madrid13-slides-Tihomir-Gvero.pptx|Synthesizing and Repairing Expressions using Types and Weights}} |
 +| 17:00 - 17:30 | Robert Koenighofer ​ | {{:​madrid13-slides-Robert-Koenighofer.pdf|QBF-Based Synthesis Methods for Safety Specifications}} |
 +| 17:30 - 18:00 | Guillermo Perez | {{:​madrid13-slides-Guillermo-Perez.pdf|Mean-payoff games: imperfect vs. incomplete information}} |
 +
 +
 +=== Friday, Oct 18 ===
 +
 +^             ^ Title                 ^ Speaker ^
 +^ SESSION 4 ^ Program Verification and Reliability (Chair: Enric Rodriguez-Carbonell) ^^
 +| 9:00-10:00 | Invited Talk : Willem Visser | {{:​madrid13-slides-Willem-Visser.ppt|Model Counting >= Symbolic Execution}} |
 +| 10:00 - 10:30 | ** Coffee break ** ||
 +| 10:30 - 11:00 | Radu Iosif | {{:​madrid13-slides-Radu-Iosif.pdf|Safety Problems are NP-complete for Flat Integer Programs with Octagonal Loops}} |
 +| 11:00 - 11:30 | Hossein Hojjat | {{:​madrid13-slides-Hossein-Hojjat.pdf|Relational Invariants for Verification of Parameterized Timed Systems}} |
 +| 11:30 - 12:00 | Dana Drachsler | {{:​madrid13-slides-Dana-Drachsler.pdf|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 | {{:​madrid13-abs-Tarmo-Uustalu.pdf|A Hoare Logic for Reasoning About Nonterminating Behaviors}} |
 +| 14:30 - 15:00 | Denis Firsov | {{:​madrid13-slides-Denis-Firsov.pdf|Formalizing Attribute Grammars and Circularity Checking}} |
 +| 15:00 - 15:30 | Adam Rogalewicz | {{:​madrid13-slides-Adam-Rogalewicz.pdf|The Tree Width of Separation Logic with Recursive Definitions}} |
 +| 15:30 - 16:00 | Gabriel Istrate | {{:​madrid13-slides-Gabriel-Istrate.pdf|From simple combinatorial statements with difficult mathematical proofs to hard instances of SAT}} |
 +| 16:00  | Closing Remarks ||
 +
 +
  
 ===== Local Arrangements ===== ===== Local Arrangements =====
Line 12: Line 58:
 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]]).