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
Last revision Both sides next revision
madrid13 [2013/09/23 15:00]
cesar.sanchez
madrid13 [2013/10/30 14:27]
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-slides-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 =====