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 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 (here). It will depart from IMDEA Software back to Madrid after the afternoon sessions.
| Speaker | Title | |
|---|---|---|
| 9:00-10:00 | Invited Talk : Cesare Tinelli | 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 | 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:30 - 12:00 | Grant Passmore | 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 | Formal Methods in Aerospace: Constraints, Assets and Challenges |
| 15:00 - 15:30 | Antti Hyvärinen | Verification-Aided Regression Testing |
| 15:30 - 16:00 | Pavle Subotic | Exploring Interpolants |
| 16:00 - 16:30 | Coffee Break | |
| SESSION 3 | Synthesis and Games (Chair: Cesar Sanchez) | |
| 16:30 - 17:00 | Tihomir Gvero | Synthesizing and Repairing Expressions using Types and Weights |
| 17:00 - 17:30 | Robert Koenighofer | QBF-Based Synthesis Methods for Safety Specifications |
| 17:30 - 18:00 | Guillermo Perez | Mean-payoff games: imperfect vs. incomplete information |
| Title | Speaker | |
|---|---|---|
| SESSION 4 | Program Verification and Reliability (Chair: Enric Rodriguez-Carbonell) | |
| 9:00-10:00 | Invited Talk : Willem Visser | Model Counting >= Symbolic Execution |
| 10:00 - 10:30 | Coffee break | |
| 10:30 - 11:00 | Radu Iosif | 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:30 - 12:00 | Dana Drachsler | 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 | A Hoare Logic for Reasoning About Nonterminating Behaviors |
| 14:30 - 15:00 | Denis Firsov | Formalizing Attribute Grammars and Circularity Checking |
| 15:00 - 15:30 | Adam Rogalewicz | 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 |
| 16:00 | Closing Remarks | |
Accommodation
The workshop will be held at the IMDEA Software Institute (see here for directions). Note that IMDEA is not near the Madrid city center and transportation is needed to commute.
The Local Orgranization will reserve a private bus that will depart in the morning from the corner between Plaza Santo Domingo and Calle Jacometrezo (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:
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 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
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 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
If you have any questions regarding logistics you can email directly Cesar Sanchez(cesar.sanchez@imdea.org) or Tania Rodriguez (tania.rodriguez@imdea.org).