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 Both sides next revision
madrid13 [2013/10/10 11:46]
cesar.sanchez
madrid13 [2013/10/10 19:28]
enric.rodriguez.carbonell
Line 8: Line 8:
  
 ^             ^ 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 30:
 ^             ^ 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 : {{:​madrid13-abs-Willem-Visser.pdf|Willem Visser | 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 ||