Colloquium-C

We consider the problem of testing whether a graph has bounded arboricity.

The family of graphs with bounded arboricity includes, among others, bounded-degree graphs, all minor-closed graph classes (e.g. planar graphs, graphs with bounded treewidth) and randomly generated preferential attachment graphs.

Graphs with bounded arboricity have been studied extensively in the past, in particular since for many problems they allow for much more efficient algorithms and/or better approximation ratios.

Recent years have shown adoption of new software trends such as machine learning, programmable computer networks, and blockchain frameworks. Several software bugs and attacks have demonstrated the importance of bringing formal guarantees to such systems. Techniques from verification, automated reasoning and program synthesis were shown successful in providing such guarantees for software systems. My research extends these techniques to these new software trends.

The goal in formal methods is to formally reason about systems. Game theory is an important tool in formal methods. A prominent application is synthesis, where we automatically construct a correct system from a given specification. Synthesis is reduced to solving a two-player game between a system player and an adversarial environment. Indeed, a correct system can be viewed as a strategy that guarantees that the specification is satisfied, no matter how the environment behaves.

The drastically growing scale of today's networks makes manag

As software has grown increasingly critical to our society’s infrastructure, mechanically-verified software has grown increasingly important, feasible, and prevalent. Proof assistants have seen tremendous growth in recent years because of their success in the mechanical verification of high-value applications in many areas, including cyber security, cyber-physical systems, operating systems, compilers, and microkernels.

We all capture the world around us through digital data such as images, videos and sound. However, in many cases, we are interested in certain properties of the data that are either not available or difficult to perceive directly from the input signal. My goal is to “Re-render Reality”, i.e., develop algorithms that analyze digital signals and then create a new version of it that allows us to see and hear better. In this talk, I’ll present a variety of methodologies aimed at enhancing the way we perceive our world through modified, re-rendered output.