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
haifa12 [2012/10/30 13:51]
eran.yahav
haifa12 [2012/11/04 15:48]
eran.yahav
Line 27: Line 27:
 Join us for a students'​ evening out the night before the conference at the historic Camel Restaurant and Cafe on one of Haifa'​s most picturesque beaches. We'll enjoy an evening of beer and refreshments as we spend time at the Camel, one of Haifa'​s most unique eateries, located on Dado Beach at the southern tip of Haifa. Join us for a students'​ evening out the night before the conference at the historic Camel Restaurant and Cafe on one of Haifa'​s most picturesque beaches. We'll enjoy an evening of beer and refreshments as we spend time at the Camel, one of Haifa'​s most unique eateries, located on Dado Beach at the southern tip of Haifa.
 see http://​www.research.ibm.com/​haifa/​conferences/​hvc2012/​social.shtml see http://​www.research.ibm.com/​haifa/​conferences/​hvc2012/​social.shtml
 +
 +
 +==== Suggested Dinner Locations ====
 +
 +seafood: ​
 +http://​www.rol.co.il/​sites/​jako-maachali-yam-haifa1/​
 +
 +meat: 
 +http://​www.sinta-bar.co.il/​site/​english.html
 +http://​meat.rest-e.co.il/​
 +
 +fancy:
 +http://​www.tripadvisor.com/​Restaurant_Review-g293982-d1595889-Reviews-Hanamal_24-Haifa_Haifa_District.html
 +
 +vegeterian:
 +http://​www.tripadvisor.com/​Restaurant_Review-g293982-d2431142-Reviews-Cafe_Louise-Haifa_Haifa_District.html
 +
 +middle-eastern:​
 +http://​www.tripadvisor.com/​Restaurant_Review-g293982-d1020765-Reviews-Fatoush-Haifa_Haifa_District.html
 +
 +local beer: 
 +http://​www.ratebeer.com/​p/​libira-haifa/​19781/​
 +
  
 ===== Registration ===== ===== Registration =====
Line 47: Line 70:
 | 14:25-14:50 | Assisted Verification of Invariance for Parametrized Systems | Alejandro Sánchez | | 14:25-14:50 | Assisted Verification of Invariance for Parametrized Systems | Alejandro Sánchez |
 | 14:50-15:15 | Interpolation for resolution and superposition | Maria Paola Bonacina | | 14:50-15:15 | Interpolation for resolution and superposition | Maria Paola Bonacina |
-| 15:15-15:40 | Reductions for Synthesis Procedures | Philippe Suter | +| 15:15-15:30 | short break || 
-| 15:40-16:05 | Logico-Numerical Max-Strategy Iteration | Pavle Subotic |  +| 15:​30-15:​55 ​| Reductions for Synthesis Procedures | Philippe Suter | 
-| 16:05-16:20 short break || +| 15:55-16:20 | Logico-Numerical Max-Strategy Iteration | Pavle Subotic |  
-| 16:20-17:30 | Management Committee Meeting ||+| 16:20-16:45 Information flow analysis and temporal logics| Markus Rabe ||  
 +| 16:45-17:00 | short break || 
 +| 17:​00-18:​00 ​| Management Committee Meeting ||
  
 ===== Invited Talks (under construction) ===== ===== Invited Talks (under construction) =====
Line 71: Line 96:
  
 Reductions for Synthesis Procedures / Philippe Suter  Reductions for Synthesis Procedures / Philippe Suter 
 +
 +Information Flow Analysis / Markus Rabe
  
 ===== Full Abstracts ===== ===== Full Abstracts =====
Line 272: Line 299:
 applicable, thus simplifying both the presentation and the correctness applicable, thus simplifying both the presentation and the correctness
 argument. argument.
 +
 +
 +----
 +**Logico-Numerical Max-Strategy Iteration**
 +//Pavle Subotic//
 +
 +Strategy iteration methods are used for solving fixed point equations.
 +It has been shown that they improve precision in static analysis based
 +on abstract interpretation
 +and template polyhedra. However, they are limited to numerical
 +programs. In this talk a method for applying max-strategy iteration to
 +logico-numerical programs is presented. This method computes the least
 +fixed point w.r.t. the abstract domain; in particular, it does not
 +resort to widening.
 +
 +(Joint work with Peter Schrammel, INRIA Grenoble)
 +
 +----
 +**Information flow analysis and temporal logics**
 +//Markus Rabe//
 +
 +Most analysis methods for information flow properties, such as noninterference,​ do not consider temporal restrictions. In practice, however, such properties rarely occur statically, but have to consider constraints such as when and under which conditions a variable has to be kept secret. I will present recent results on how to integrate information flow properties into temporal logics by introducing a new modal operator. ​
 +Finally, I will sketch upcoming work on integrating information flow properties in game logics such as ATL*.