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/10/10 11:46]
cesar.sanchez
madrid13 [2013/10/14 18:21]
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. ​
 +
 +===== 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 ===== ===== PROGRAMME =====
Line 8: Line 12:
  
 ^             ^ Speaker ​                ^ Title ^ ^             ^ Speaker ​                ^ Title ^
-| 9:00-10:00 | Invited Talk : Cesare Tinelli |Solving quantified formulas in SMT by finite model finding |+| 9:00-10:00 | Invited Talk : Cesare Tinelli ​| {{:​madrid13-abs-Cesare-Tinelli.pdf|Solving quantified formulas in SMT by finite model finding}} |
 | 10:00 - 10:30 | ** Coffee break ** || | 10:00 - 10:30 | ** Coffee break ** ||
 ^ SESSION 1 ^ SAT and SMT + Applications (Chair: Maria Paola Bonacina) ^^ ^ 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 | +| 10:30 - 11:00 | Eivind Jahren ​| {{:​madrid13-abs-Eivind-Jahren.pdf|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:00 - 11:30 | Predrag Janicic ​| {{:​madrid13-abs-Predrag-Janicic.pdf|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 |+| 11:30 - 12:00 | Grant Passmore ​| {{:​madrid13-abs-Grant-Passmore.pdf|Exact Global Nonlinear Optimization on Demand}} |
 | 12:00 - 14:00 | ** Lunch ** || | 12:00 - 14:00 | ** Lunch ** ||
 ^  SESSION 2 ^ Formal Methods, Verification and Model Checking (Chair: Radu Iosif) ^^  ^  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 | +| 14:00 - 15:00 | Invited talk : Virginie Wiels | {{:​madrid13-abs-Virginie-Wiels.pdf|Formal Methods in Aerospace: Constraints,​ Assets and Challenges}} 
-| 15:00 - 15:30 | Antti Hyvärinen | Verification-Aided Regression Testing | +| 15:00 - 15:30 | Antti Hyvärinen ​| {{:​madrid13-abs-Antti-Hyvärinen.pdf|Verification-Aided Regression Testing}} 
-| 15:30 - 16:00 | Pavle Subotic | Exploring Interpolants |+| 15:30 - 16:00 | Pavle Subotic ​| {{:​madrid13-abs-Pavle-Subotic.pdf|Exploring Interpolants}} |
 | 16:00 - 16:30 | ** Coffee Break ** || | 16:00 - 16:30 | ** Coffee Break ** ||
 ^  SESSION 3 ^ Synthesis and Games (Chair: Cesar Sanchez) ^^ ^  SESSION 3 ^ Synthesis and Games (Chair: Cesar Sanchez) ^^
-| 16:30 - 17:00 | Tihaomir ​Gvero | Synthesizing and Repairing Expressions using Types and Weights | +| 16:30 - 17:00 | Tihomir ​Gvero | {{:​madrid13-abs-Tihomir-Gvero.pdf|Synthesizing and Repairing Expressions using Types and Weights}} 
-| 17:00 - 17:30 | Robert Koenighofer ​ | QBF-Based Synthesis Methods for Safety Specifications | +| 17:00 - 17:30 | Robert Koenighofer  ​| {{:​madrid13-abs-Robert-Koenighofer.pdf|QBF-Based Synthesis Methods for Safety Specifications}} 
-| 17:30 - 18:00 | Guillermo Perez | Mean-payoff games: imperfect vs. incomplete information |+| 17:30 - 18:00 | Guillermo Perez | {{:​madrid13-abs-Guillermo-Perez.pdf|Mean-payoff games: imperfect vs. incomplete information}} |
  
  
Line 30: Line 34:
 ^             ^ Title                 ^ Speaker ^ ^             ^ Title                 ^ Speaker ^
 ^ SESSION 4 ^ Program Verification and Reliability (Chair: Enric Rodriguez-Carbonell) ^^ ^ SESSION 4 ^ Program Verification and Reliability (Chair: Enric Rodriguez-Carbonell) ^^
-| 9:00-10:00 | Invited Talk : Willem Visser | Model Counting >= Symbolic Execution |+| 9:00-10:00 | Invited Talk : Willem Visser ​| {{:​madrid13-abs-Willem-Visser.pdf|Model Counting >= Symbolic Execution}} |
 | 10:00 - 10:30 | ** Coffee break ** || | 10:00 - 10:30 | ** Coffee break ** ||
-| 10:30 - 11:00 | Radu Iosif | Safety Problems are NP-complete for Flat Integer Programs with Octagonal Loops | +| 10:30 - 11:00 | Radu Iosif | {{:​madrid13-abs-Radu-Iosif.pdf|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:00 - 11:30 | Hossein Hojjat ​| {{:​madrid13-abs-Hossein-Hojjat.pdf|Relational Invariants for Verification of Parameterized Timed Systems}} 
-| 11:30 - 12:00 | Dana Drachsler | A Verification-Friendly Concurrent Binary Tree |+| 11:30 - 12:00 | Dana Drachsler ​| {{:​madrid13-abs-Dana-Drachsler.pdf|A Verification-Friendly Concurrent Binary Tree}} |
 ^ 12:00 - 14:00 ^ ** BUSINESS MEETING / LUNCH ** ^^ ^ 12:00 - 14:00 ^ ** BUSINESS MEETING / LUNCH ** ^^
 ^  SESSION 5 ^ Logics, Formal Languages and Semantics (Chair: Predrag Janicic) ^^  ^  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:00 - 14:30 | Tarmo Uustalu ​| {{:​madrid13-abs-Tarmo-Uustalu.pdf|A Hoare Logic for Reasoning About Nonterminating Behaviors}} 
-| 14:30 - 15:00 | Denis Firsov | Formalizing Attribute Grammars and Circularity Checking | +| 14:30 - 15:00 | Denis Firsov ​| {{:​madrid13-abs-Denis-Firsov.pdf|Formalizing Attribute Grammars and Circularity Checking}} 
-| 15:00 - 15:30 | Adam Rogalewicz | The Tree Width of Separation Logic with Recursive Definitions | +| 15:00 - 15:30 | Adam Rogalewicz ​| {{:​madrid13-abs-Adam-Rogalewicz.pdf|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 |+| 15:30 - 16:00 | Gabriel Istrate ​| {{:​madrid13-abs-Gabriel-Istrate.pdf|From simple combinatorial statements with difficult mathematical proofs to hard instances of SAT}} |
 | 16:00  | Closing Remarks || | 16:00  | Closing Remarks ||