Witnessing Program Transformations

  • Namjoshi K.
  • Zuck L.

We study two closely related problems: (a) showing that a program transformation is correct and (b) propagating a program invariant through a sequence of transformations. The second problem is motivated by an application where invariants on a program are used to enhance both the scope and the quality of the optimizations applied during compilation. We show that both problems can be addressed by generating, at compile-time, a witness for every instance of a transformation. A witness may be checked independently to establish the correctness of the transformation and, if correct, a witness helps transfer invariants from the source to the target program. This approach is simpler than proving correctness of the transformation over all inputs, and more comprehensive than translation validation heuristics, which are limited to specific transformations. We prove that stuttering simulation is a complete witness format: every correct transformation has a witness that is a stuttering simulation relation. Moreover, stuttering simulation witnesses compose, resulting in a single witness for a sequence of transformations. We define simulation witnesses for a number of standard compiler optimizations; this exercise indicates that witness generation is usually much simpler than the corresponding optimization procedure.

Recent Publications

August 09, 2017

A Cloud Native Approach to 5G Network Slicing

  • Francini A.
  • Miller R.
  • Sharma S.

5G networks will have to support a set of very diverse and often extreme requirements. Network slicing offers an effective way to unlock the full potential of 5G networks and meet those requirements on a shared network infrastructure. This paper presents a cloud native approach to network slicing. The cloud ...

August 01, 2017

Modeling and simulation of RSOA with a dual-electrode configuration

  • De Valicourt G.
  • Liu Z.
  • Violas M.
  • Wang H.
  • Wu Q.

Based on the physical model of a bulk reflective semiconductor optical amplifier (RSOA) used as a modulator in radio over fiber (RoF) links, the distributions of carrier density, signal photon density, and amplified spontaneous emission photon density are demonstrated. One of limits in the use of RSOA is the lower ...

July 12, 2017

PrivApprox: Privacy-Preserving Stream Analytics

  • Chen R.
  • Christof Fetzer
  • Le D.
  • Martin Beck
  • Pramod Bhatotia
  • Thorsten Strufe

How to preserve users' privacy while supporting high-utility analytics for low-latency stream processing? To answer this question: we describe the design, implementation and evaluation of PRIVAPPROX, a data analytics system for privacy-preserving stream processing. PRIVAPPROX provides three properties: (i) Privacy: zero-knowledge privacy (ezk) guarantees for users, a privacy bound tighter ...