Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
haifa12 [2012/10/29 11:43] – eran.yahavhaifa12 [2012/11/18 08:07] (current) – eran.yahav
Line 28: Line 28:
 see http://www.research.ibm.com/haifa/conferences/hvc2012/social.shtml see http://www.research.ibm.com/haifa/conferences/hvc2012/social.shtml
  
-===== Registration ===== 
-To register please send email with your name and affiliation to [[noafr@cs.technion.ac.il|noafr@cs.technion.ac.il]] 
  
-**Please also register to [[http://www.research.ibm.com/haifa/conferences/hvc2012/registration.shtml|HVC]]. If you are only attending the COST meeting - register for the tutorials day only. +==== Suggested Dinner Locations ====
-We need the HVC registration to arrange parking, lunches, and wifi connections.** +
  
 +seafood: 
 +http://www.rol.co.il/sites/jako-maachali-yam-haifa1/
  
-===== Schedule =====+meat:  
 +http://www.sinta-bar.co.il/site/english.html 
 +http://meat.rest-e.co.il/
  
-^       ^ Title       ^ Speaker          ^ +fancy: 
-| 10:00-10:45 | Quantitative Abstraction Refinement | Pavol Cerny (invited talk) | +http://www.tripadvisor.com/Restaurant_Review-g293982-d1595889-Reviews-Hanamal_24-Haifa_Haifa_District.html
-| 10:45-11:30 | PINCETTE project: validation of changes and upgrades in large software systems | Hana Chockler (invited talk) | +
-| 11:30-11:45 | short break || +
-| 11:45-12:15 | Finite-State and Pushdown Games with Multi-dimensional Mean-Payoff Objectives | Yaron Velner | +
-| 12:15-12:45 | Privacy for Linked Data | Silvia Ghilezan |  +
-| 12:45-14:00 | Lunch Break || +
-| 14:00-14:30 | Interpolant Strength in Model Checking | Simone Rollini | +
-| 14:30-15:00 | Assisted Verification of Invariance for Parametrized Systems | Alejandro Sánchez | +
-| 15:00-15:30 | Interpolation for resolution and superposition | Maria Paola Bonacina | +
-| 15:30-16:00 | Reductions for Synthesis Procedures | Philippe Suter | +
-| 16:00-16:15 | short break || +
-| 16:15-17:30 | Management Committee Meeting ||+
  
-===== Invited Talks (under construction) =====+vegeterian: 
 +http://www.tripadvisor.com/Restaurant_Review-g293982-d2431142-Reviews-Cafe_Louise-Haifa_Haifa_District.html
  
-Quantitative Abstraction Refinement / Pavol Cerny+middle-eastern: 
 +http://www.tripadvisor.com/Restaurant_Review-g293982-d1020765-Reviews-Fatoush-Haifa_Haifa_District.html
  
-PINCETTE project: validation of changes and upgrades in large software systems - unique challenges and suggested solutions / Hana Chockler+local beer:  
 +http://www.ratebeer.com/p/libira-haifa/19781/
  
-===== Talks (under construction) ===== 
  
-Finite-State and Pushdown Games with Multi-dimensional Mean-Payoff Objectives / Yaron Velner+===== Registration ===== 
 +To register please send email with your name and affiliation to [[noafr@cs.technion.ac.il|noafr@cs.technion.ac.il]]
  
-Privacy for Linked Data / Silvia Ghilezan+**Please also register to [[http://www.research.ibm.com/haifa/conferences/hvc2012/registration.shtml|HVC]]. If you are only attending the COST meeting - register for the tutorials day only. 
 +We need the HVC registration to arrange parking, lunches, and wifi connections.** 
  
-Interpolant Strength in Model Checking / Simone Rollini 
  
-Assisted Verification of Invariance for Parametrized Systems / Alejandro Sánchez+===== Schedule ===== 
 + 
 +^       ^ Title       ^ Speaker          ^ 
 +| 10:00-10:45 | {{:haifa12-pvaol.ppt|Quantitative Abstraction Refinement}}| Pavol Cerny (invited talk) | 
 +| 10:45-11:30 | {{:haifa12-hana.ppt|PINCETTE project: validation of changes and upgrades in large software systems}} | Hana Chockler (invited talk) | 
 +| 11:30-11:45 | short break || 
 +| 11:45-12:10 | Finite-State and Pushdown Games with Multi-dimensional Mean-Payoff Objectives | Yaron Velner | 
 +| 12:10-12:35 | Privacy for Linked Data | Silvia Ghilezan |  
 +| 12:35-14:00 | Lunch Break || 
 +| 14:00-14:25 | {{:haifa12-simone.pdf|Interpolant Strength in Model Checking}} | Simone Rollini | 
 +| 14:25-14:50 | {{:haifa12-asanchez.pdf|Assisted Verification of Invariance for Parametrized Systems}} | Alejandro Sánchez | 
 +| 14:50-15:15 | {{:haifa12-maria.pdf|Interpolation for resolution and superposition}} | Maria Paola Bonacina | 
 +| 15:15-15:30 | short break || 
 +| 15:30-15:55 | {{:haifa12-philippe.pdf|Reductions for Synthesis Procedures}} | Philippe Suter | 
 +| 15:55-16:20 | {{:haifa12-pvale.pdf|Logico-Numerical Max-Strategy Iteration}} | Pavle Subotic |  
 +| 16:20-16:45 | {{:haifa12-markus.pdf|Information flow analysis and temporal logics}} | Markus Rabe ||  
 +| 16:45-17:00 | short break || 
 +| 17:00-18:00 | Management Committee Meeting || 
 + 
 +===== Invited Talks  =====
  
-Interpolation for resolution and superposition / Maria Paola Bonacina+**Pavol Cerny**: Quantitative Abstraction Refinement by 
  
-Reductions for Synthesis Procedures / Philippe Suter +**Hana Chockler**: PINCETTE project: validation of changes and upgrades in large software systems - unique challenges and suggested solutions 
  
-===== Full Abstracts =====+===== Talk Abstracts =====
  
 **Quantitative Abstraction Refinement** **Quantitative Abstraction Refinement**
Line 271: Line 283:
 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*.