Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
madrid13 [2013/10/14 18:21] cesar.sanchez |
madrid13 [2013/11/11 07:59] (current) enric.rodriguez.carbonell |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| 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 ===== | + | ===== 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. | 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. | ||
| Line 12: | Line 12: | ||
| ^ ^ Speaker ^ Title ^ | ^ ^ Speaker ^ Title ^ | ||
| - | | 9:00-10:00 | Invited Talk : Cesare Tinelli | {{:madrid13-abs-Cesare-Tinelli.pdf|Solving quantified formulas in SMT by finite model finding}} | | + | | 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 ** || | | 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 | {{:madrid13-abs-Eivind-Jahren.pdf|Maintenance Scheduling in the Oil Industry Using SMT Techniques}} | | + | | 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-abs-Predrag-Janicic.pdf|Proving Correctness of a KRK Chess Endgame Strategy by SAT-Based Constraint Solving}} | | + | | 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-abs-Grant-Passmore.pdf|Exact Global Nonlinear Optimization on Demand}} | | + | | 11:30 - 12:00 | Grant Passmore | {{:madrid13-slides-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 | {{:madrid13-abs-Virginie-Wiels.pdf|Formal Methods in Aerospace: Constraints, Assets and Challenges}} | | + | | 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-abs-Antti-Hyvärinen.pdf|Verification-Aided Regression Testing}} | | + | | 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}} | | + | | 15:30 - 16:00 | Pavle Subotic | {{:madrid13-slides-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 | Tihomir Gvero | {{:madrid13-abs-Tihomir-Gvero.pdf|Synthesizing and Repairing Expressions using Types and Weights}} | | + | | 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-abs-Robert-Koenighofer.pdf|QBF-Based Synthesis Methods for Safety Specifications}} | | + | | 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-abs-Guillermo-Perez.pdf|Mean-payoff games: imperfect vs. incomplete information}} | | + | | 17:30 - 18:00 | Guillermo Perez | {{:madrid13-slides-Guillermo-Perez.pdf|Mean-payoff games: imperfect vs. incomplete information}} | |
| Line 34: | 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 | {{:madrid13-abs-Willem-Visser.pdf|Model Counting >= Symbolic Execution}} | | + | | 9:00-10:00 | Invited Talk : Willem Visser | {{:madrid13-slides-Willem-Visser.ppt|Model Counting >= Symbolic Execution}} | |
| | 10:00 - 10:30 | ** Coffee break ** || | | 10:00 - 10:30 | ** Coffee break ** || | ||
| - | | 10:30 - 11:00 | Radu Iosif | {{:madrid13-abs-Radu-Iosif.pdf|Safety Problems are NP-complete for Flat Integer Programs with Octagonal Loops}} | | + | | 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-abs-Hossein-Hojjat.pdf|Relational Invariants for Verification of Parameterized Timed Systems}} | | + | | 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-abs-Dana-Drachsler.pdf|A Verification-Friendly Concurrent Binary Tree}} | | + | | 11:30 - 12:00 | Dana Drachsler | {{:madrid13-slides-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 | {{:madrid13-abs-Tarmo-Uustalu.pdf|A Hoare Logic for Reasoning About Nonterminating Behaviors}} | | + | | 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-abs-Denis-Firsov.pdf|Formalizing Attribute Grammars and Circularity Checking}} | | + | | 14:30 - 15:00 | Denis Firsov | {{:madrid13-slides-Denis-Firsov.pdf|Formalizing Attribute Grammars and Circularity Checking}} | |
| - | | 15:00 - 15:30 | Adam Rogalewicz | {{:madrid13-abs-Adam-Rogalewicz.pdf|The Tree Width of Separation Logic with Recursive Definitions}} | | + | | 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-abs-Gabriel-Istrate.pdf|From simple combinatorial statements with difficult mathematical proofs to hard instances of SAT}} | | + | | 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 || | | 16:00 | Closing Remarks || | ||