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
haifa12 [2012/10/29 11:39]
eran.yahav
haifa12 [2012/11/18 08:07] (current)
eran.yahav
Line 20: Line 20:
 see the [[http://​www.research.ibm.com/​haifa/​conferences/​hvc2012/​|HVC]] page: http://​www.research.ibm.com/​haifa/​conferences/​hvc2012/​info.shtml see the [[http://​www.research.ibm.com/​haifa/​conferences/​hvc2012/​|HVC]] page: http://​www.research.ibm.com/​haifa/​conferences/​hvc2012/​info.shtml
  
 +==== Social Events (HVC) ====
  
 +**Student'​s night out!**
 +Time: Nov. 5, 19:00
 +Place: "The Camel" on the Haifa beach
 +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
  
-===== 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 (under construction) =====+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 projectvalidation 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 265: 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*.