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
madrid13 [2013/09/23 15:00]
cesar.sanchez
madrid13 [2013/11/11 07:59]
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-slides-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 =====