Differences

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

--- haifa12 [2012/10/15 14:07]
eran.yahav
+++ haifa12 [2012/11/18 08:07]
eran.yahav
@@ Line 6: / Line 6: @@
 For more information, please contact [[http://www.cs.technion.ac.il/~yahave/|Eran Yahav]] and [[http://fmv.jku.at/biere/|Armin Biere]].
+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, [[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 14: / Line 18: @@
 ==== 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
+==== 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
+==== 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 =====
 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.
+We need the HVC registration to arrange parking, lunches, and wifi connections.**
-===== Invited Talks (under construction) =====
-Quantitative Abstraction Refinement / Pavol Cerny
+===== Schedule =====
-PINCETTE project: validation of changes and upgrades in large software systems - unique challenges and suggested solutions / Hana Chockler
+^       ^ 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 ||
-===== Talks (under construction) =====
+===== Invited Talks  =====
-Finite-State and Pushdown Games with Multi-dimensional Mean-Payoff Objectives / Yaron Velner
+**Pavol Cerny**: Quantitative Abstraction Refinement by
-Privacy for Linked Data / Silvia Ghilezan
+**Hana Chockler**: PINCETTE project: validation of changes and upgrades in large software systems - unique challenges and suggested solutions
+===== Talk Abstracts =====
-===== Full Abstracts =====
 **Quantitative Abstraction Refinement**
@@ Line 149: / Line 199: @@
 ----
+**Interpolant Strength in Model Checking**
+//Simone Rollini//
+Craig interpolation is a well known method of abstraction successfully used in both hardware and software model checking.  The logical strength of interpolants can affect the quality of approximations and consequently the performance of the model checkers. Recently, it was observed that for the same resolution proof a complete lattice of interpolants ordered by strength can be derived.
+Most state-of-the-art model checking techniques based on interpolation subject the interpolants
+to constraints that ensure efficient verification as, for example, in transition relation approximation for bounded model checking, counterexample-guided abstraction refinement and function summarization for software update checking. However, in general, these verification-specific constraints are not satisfied by all possible interpolants.
+We analyze the restrictions within the lattice of interpolants under which the required constraints are satisfied.  This enables investigation of the effect of the strength of interpolants on the particular techniques, while preserving their soundness.
+(Joint work with Ondrej Sery and Natasha Sharygina)
+----
+**Assisted Verification of Invariance for Parametrized Systems**
+//Alejandro Sánchez//
+We study the verification of safety properties over symmetric
+parametrized systems. These systems consist on an arbitrary and
+unbounded number of threads running the same program. In this
+scenario, following standard deductive techniques leads to the need of
+verifying an unbounded collection of verification conditions which
+grows with the number of threads involved in the system. To handle
+this problem, we present a technique based on parametrized invariance
+rules to reduce the verification of finite and infinite state
+parametrized programs to the analysis of only a finite number of
+verification conditions. In our approach, all necessary VCs are
+automatically generated from the program and its specification,
+independently of the number of threads involved in the system.
+In this talk, we present the latest advances in our research as well
+as some running examples including a ticket-based mutual exclusion
+algorithm and a concurrent single-linked list implementation. Both
+examples are verified using Leap. Leap is a tool under development at
+the IMDEA Software Institute which implements the parametrized
+invariance rules. Our tool is able to automatically generate all
+necessary VCs starting from the program and the properties
+specifications. Leap also implements decision procedures to
+automatically verify VCs, and is also extended to interactively assist
+the user in the verification process. Currently, the decision
+procedures allow to programs that manipulate numbers, sets, list
+layouts and their combinations, built on top of state-of-the-art SMT
+solvers.
+(joint work with César Sánchez)
+----
+**Interpolation for resolution and superposition**
+//Maria Paola Bonacina//
+Given two inconsistent formulae, a (reverse) interpolant is a
+formula implied by one, inconsistent with the other and only
+containing symbols they share. Interpolants are used in
+verification to compute over-approximations of images, refine
+abstractions, or generate invariants. We consider interpolation
+of refutations generated by inference systems for first-order
+logic with equality, with resolution and superposition. These
+inference systems are at the heart of state-of-the-art theorem
+provers, may yield decision procedures, and can be integrated
+in SMT-solvers. We present a two-stage approach that computes
+provisional interpolants, which may contain non-shared symbols,
+and applies lifting to replace them with quantified variables.
+The resulting interpolation system is complete, meaning that
+it extracts an interpolant from any refutation.
+(Joint work with Moa Johansson)
+----
+**Reductions for Synthesis Procedures**
+//Philippe Suter//
+A synthesis procedure acts as a compiler for declarative
+specifications. It accepts a formula describing a relation between
+inputs and outputs, and generates a function implementing this relation.
+This paper presents synthesis procedures for data structures. Our
+procedures are reductions that lift a synthesis procedure for the
+elements into synthesis procedures for containers storing these
+elements. We introduce a framework to describe synthesis procedures as
+systematic applications of inference rules. We show that, by
+interpreting both synthesis problems and programs as relations, we can
+derive and modularly prove transformation rules that are widely
+applicable, thus simplifying both the presentation and the correctness
+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*.