Below are some of the on-going projects in our group. Most of these involve some combination of theory (e.g. program analysis, synthesis) and practice (e.g. concurrent algorithms, web vulnerabilities).
Under each of these projects, we have a number of available B.Sc., M.Sc. and Ph.D. thesis topics ranging from more theoretical to systems building. If you are interested, please drop us a line.
Statistical Techniques for Program Reasoning
In this project we investigate new directions for automating common programming tasks by combining classic program analysis with statistical techniques (e.g. language models, machine translation). The basic idea is to learn from the massive amount of code already available on the Web in order to perform various tasks, such as migrating programs from one language to another, automatically synthesizing new code and even predicting programming errors before they actually occur.
Synthesis from Examples
For many programming tasks, it is far easier for a developer to provide their intent via examples of what a program should do, rather than write the whole program from scratch or to write formal logical specifications. In this project we investigate various research directions for automatically synthesizing programs from examples. These range from code search, to refactoring and even to the discovery of data structure algorithms. Many of these approaches combine several techniques, including program analysis, SMT solvers, data mining and machine learning.
In this direction we collaborate with several groups, including Technion (Israel), IBM T.J. Watson Research Center (USA) and NTU (Singapore).
Analysis of Event-Driven Applications
Many end-user applications such as web sites and smartphone apps are written in an event-driven style. Unfortunately, these applications can exhibit incorrect behaviors fundamentally caused by the incorrect handling of asynchrony that arises from the application's interaction with the external world (e.g. user clicks, network interrupts, etc).
In this project, we develop new program analysis techniques (based on dynamic analyiss and graph algorithms) that can detect and correct such issues automatically in real-world applications (e.g. Google Maps).
The project is a collaboration between ETH Zurich and the IBM T.J. Watson Research Center.
See web site for more details.
Analysis and Synthesis for Relaxed Memory Models
To improve performance, virtually all modern processers (e.g. Intel) support relaxed memory models. Unfortunately, programming these relaxed models is difficult and error-prone, yet highly desirable for systems software (e.g. the Linux kernel, concurrent algorithms).
In this project, we develop new automated program analysis (e.g. predicate abstraction, abstract interpretation, model checking) and synthesis techniques which enable us to build systems software that exploits these chips corrrectly and efficiently.
The project is a collaboration between ETH Zurich and Technion.
See web site for more details.
Analysis of Structured Parallel Programs
Programming languages are increasingly adopting some form of structured parallelism in order to manage the complexity of writing parallel programs (e.g. X10, Cilk, Scala, F#, GPU CUDA kernels, etc). In this project we develop program analysis algorithms that analyze such structured programs. These program analyzers aim to leverage the structure in order to obtain better space and time complexity than analyzers for unstructured parallelism.
Practical Lower Bounds for Concurrent Algorithms
Concurrent programming involves a delicate balance between correctness and efficiency: using too much synchronization leads to inefficiency, using too little produces incorrect programs. Here, we define a wide class of concurrent programs and prove that any program in this class must use certain synchronization, or it is incorrect. These results are particularly important when it comes to libraries (e.g. Java collections), systems programming (e.g. Linux kernel) and modern processors architectures (e.g. PowerPC, Intel, ARM).
Papers: POPL'11, POPL'11 Talk: PDF, PPT, Linux Weekly News features the result
Paraglide: Synthesis of Concurrent Systems Software
In this project, we explored new directions for computer assisted construction of concurrent systems. The work ranged from new techniques for automatic synchronization inference based on semantic search to verification-driven synthesis combining program analysis and inference, to synthesis of concurrent algorithms such as concurrent data structures. Using the techniques developed here, we managed to synthesize new concurrent set and memory management algorithms which surprised even algorithmic experts. This project won the A-level Outstanding Project Award at IBM Research.
Quality Virtual Machine
The goal of this project was to scale important dynamic program analysis algorithms (e.g. resource usage) by integrating the analysis with the language runtime (i.e., the virtual machine). By making the runtime aware of the analysis, various performance optimizations are now made possible: fine-grained feedback-directed control of the analysis overhead, efficient snapshot algorithms, etc. Among other things, we extended a real-world Java VM (IBM's J9) with various analyzers as well as techniques to control the overhead (the resulting system was called QVM). Using QVM, we were able to analyze massive applications (without any change to the application) and find and repair errors that would have been very difficult or impossible to detect otherwise.