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/19 16:33]
eran.yahav
haifa12 [2012/11/18 08:07] (current)
eran.yahav
Line 9: Line 9:
 On Monday, November 5th, [[http://​workshop.ee.technion.ac.il/​|INTEL’S ANNUAL SYMPOSIUM ON VLSI CAD AND VALIDATION]] takes place at Technion. On Monday, November 5th, [[http://​workshop.ee.technion.ac.il/​|INTEL’S ANNUAL SYMPOSIUM ON VLSI CAD AND VALIDATION]] takes place at Technion.
  
-On November 6-8, HVC takes place at IBM [[http://​www.research.ibm.com/​haifa/​haifa_facility.shtml|Haifa Research Lab]] +On November 6-8, [[http://​www.research.ibm.com/​haifa/​conferences/​hvc2012/​|HVC]] takes place at IBM [[http://​www.research.ibm.com/​haifa/​haifa_facility.shtml|Haifa Research Lab]] 
  
  
Line 18: Line 18:
 ==== Hotels ==== ==== Hotels ====
  
-see the 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
  
-===== Registration ​===== +==== Social Events (HVC) ====
-To register please send email with your name and affiliation to [[noafr@cs.technion.ac.il|noafr@cs.technion.ac.il]]+
  
 +**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
  
-===== Invited Talks (under construction) ===== 
  
-Quantitative Abstraction Refinement / Pavol Cerny+==== Suggested Dinner Locations ====
  
-PINCETTE projectvalidation of changes and upgrades in large software systems ​unique challenges and suggested solutions ​Hana Chockler+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 ===== 
 +To register please send email with your name and affiliation to [[noafr@cs.technion.ac.il|noafr@cs.technion.ac.il]]
  
-===== Talks (under construction) =====+**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.** ​
  
-Finite-State and Pushdown Games with Multi-dimensional Mean-Payoff Objectives / Yaron Velner 
  
-Privacy for Linked Data / Silvia Ghilezan+===== Schedule =====
  
-Interpolant Strength in Model Checking ​Simone Rollini+^       ^ 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 ||
  
-Assisted Verification of Invariance for Parametrized Systems / Alejandro Sánchez+===== 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 244: 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*.