This is an old revision of the document!

Final COST Action Meeting, Madrid, October 17-18, 2013

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.

Thursday, Oct 17

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

Friday, Oct 18

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
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


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 : .

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( or Tania Rodriguez (