- Post Doctoral
MIT Unit Affiliation:
- Electrical Engineering & Computer Science
Post Doc Sponsor / Advisor:
Date PhD Completed:
Top 3 Areas of Expertise:
My goal is to contribute to a more disciplined approach to software by developing the theory and the tools that will be used to produce more reliable software. I have focused my work on the verification of concurrent message-passing systems and heap-manipulating programs. During one project, I worked on the programming language used to develop and verify part of the USB stack that ships with Windows 8. The succes of this project came by giving the programmer abstractions that makes them productive and enables us to apply verification. Therefore, I currently working on domain specific langues with built-in verification support. By developping verification technologies that integrates early in the software engineering process, I hope to circumvent the complexity barrier that limits the application of verification technologies and have a greater impact.
Expected End Date of Post Doctoral Position:
Programming in the physical world.
At a time when affordable 3D printer and microcontrollers give hobbyist the capability of building robots, we want to rethink these simple robots are build and programed. Being open systems, controllers are hard to test or verify on their own since they only are complete when operating on a robot. To know the effect of setting an output signal we need to know the actuator connected to it and how that affects the robot. Therefore, we are investigating how to blend together code that both controls the robot and describes it as a physical object. The code should not only easily link the inputs and outputs of the controller to the sensors and actuator, but it should also give use the kinetic and dynamic of the robot. The goal is to unify within the same framework ideas which now exists in different communities. An programming language for the logic and for the physical part, a mix of constructive solid geometry and bond graphs. Constructive solid geometry is good at describing shapes and bond graphs gives the dynamic of the system. Blending those ideas into an unified framework promise to simplify the development of robots and opens new possibilities for testing and verifying them.
DSL for distributed fault-tolerant algorithms.
Fault-tolerant distributed systems play an important role in many critical applications such as resource management in data centers. However, concurrency, uncertain message delays, and the occurrence of faults make those systems hard to design, implement, and verify. We are developing a framework for writing and verifying high-level implementations of fault-tolerant distributed algorithms. Our framework provides communication-closed rounds as primitive, which both simplifies the implementation of the fault-tolerant systems, and makes them more amenable to automated verification. By adopting communication-closed rounds, we also narrow the existing gap between the distributed algorithms literature, which often uses this abstraction, and the implementation. Furthermore, communication-closed rounds simplify the verification problem as the rounds limit the interleavings we need to consider and the communication closure allow us to remove the channels from the state-space.
Motivated by the analysis of highly dynamic message-passing systems, i.e. unbounded thread creation, mobility, etc. We present a framework for the analysis of depth-bounded systems. Depth-bounded systems are one of the most expressive known fragment of the pi-calculus for which interesting verification problems are still decidable. Even though they are infinite state systems depth-bounded systems are well-structured, thus can be analyzed algorithmically. We give an interpretation of depth-bounded systems as graph-rewriting systems. This gives more exibility and ease of use to apply depth-bounded systems to other type of systems like shared memory concurrency.
First, we develop an adequate domain of limits for depth-bounded systems, a prerequisite for the effective representation of downward-closed sets. Downward-closed sets are needed by forward saturation-based algorithms to represent potentially infinite sets of states. Then, we present an abstract interpretation framework to compute the covering set of well-structured transition systems Because, in general, the covering set is not computable, our abstraction over-approximates the actual covering set. Our abstraction captures the essence of acceleration based-algorithms while giving up enough precision to ensure convergence. We have implemented the analysis in the Picasso tool and show that it is accurate in practice. Finally, we build some further analyses like termination using the covering set as starting point.
Top 5 Awards and honors (name of award, date received):
5 Recent Papers:
Ankush Desai, Vivek Gupta, Ethan K. Jackson, Shaz Qadeer, Sriram K. Rajamani, and Damien Zufferey. (2013), “P: safe asynchronous event-driven programming”. ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’13.
Ruzica Piskac, Thomas Wies, and Damien Zufferey. (2014). “Automating Separation Logic with Trees and Data”. Computer Aided Verification - 26th International Conference, CAV 2014.
Ruzica Piskac, Thomas Wies, and Damien Zufferey. (2013), “Automating Separation Logic Using SMT”. Computer Aided Verification - 25th International Conference, CAV 2013.
Cezara Drăgoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, and Damien Zufferey. (2014), “A Logic-Based Framework for Verifying Consensus Algorithms”. Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014.
Ruzica Piskac, Thomas Wies, and Damien Zufferey. (2014), “GRASShopper: Complete Heap Verification with Mixed Specifications”. Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014.