P : Modular and Safe Event-Driven Programming
Speaker
Ankush Desai
EECS Department - UC Berkeley
Host
Michael Carbin
CSAIL CONFERENCE ROOM, 32-D463
Abstract:
Asynchronous event-driven systems are ubiquitous across domains such as distributed systems, device drivers, and robotic systems. These systems are notoriously hard to get right as the programmer needs to reason numerous control paths resulting from the myriad interleaving of events (messages) and failures.
In this talk, I will present the P language for modular and safe event-driven programming. P unifies modeling and programming into one activity for the programmer. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P also supports a module system that enables compositional (assume-guarantee) and hierarchical (refinement) reasoning of event-driven programs. Not only can a P program be compiled into executable code, but it can also be validated using state-of-the-art systematic testing (e.g., using search prioritization and symbolic execution). Using P's module system one can scale systematic testing to large, industrial-scale implementations by decomposing the system-level testing problem into a collection of simpler component-level testing problems.
P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. More recently, we have used P for the design and implementation of fault-tolerant distributed systems and robotics systems with safety-assurance.
P language: https://github.com/p-org/P
Bio:
Ankush Desai is a Ph.D. student in the EECS department at UC Berkeley working with Prof. Sanjit Seshia and Dr. Shaz Qadeer. His research focuses on designing tools and techniques in the area of programming languages, formal methods, and software engineering, and applying them to build reliable systems across domains like device drivers, distributed systems, robotics, and cyber-physical systems.
His research has had an impact both in Industry and Academia for which he was awarded the Sevin Rosen Funds Award for Innovation in 2018.
Before joining the graduate school, Ankush spent 2+ years at Microsoft Research (India) working with Dr. Sriram Rajamani and Dr. Shaz Qadeer applying formal methods to build reliable device drivers.
At IIT Kanpur, he was part of the team that built the first Indian Nano-Satellite JUGNU (launched on 12 October 2011). As a part of his Master's thesis, he designed and implemented the software stack for the on-board computer of the satellite.
Abstract:
Asynchronous event-driven systems are ubiquitous across domains such as distributed systems, device drivers, and robotic systems. These systems are notoriously hard to get right as the programmer needs to reason numerous control paths resulting from the myriad interleaving of events (messages) and failures.
In this talk, I will present the P language for modular and safe event-driven programming. P unifies modeling and programming into one activity for the programmer. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P also supports a module system that enables compositional (assume-guarantee) and hierarchical (refinement) reasoning of event-driven programs. Not only can a P program be compiled into executable code, but it can also be validated using state-of-the-art systematic testing (e.g., using search prioritization and symbolic execution). Using P's module system one can scale systematic testing to large, industrial-scale implementations by decomposing the system-level testing problem into a collection of simpler component-level testing problems.
P has been used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. More recently, we have used P for the design and implementation of fault-tolerant distributed systems and robotics systems with safety-assurance.
P language: https://github.com/p-org/P
Bio:
Ankush Desai is a Ph.D. student in the EECS department at UC Berkeley working with Prof. Sanjit Seshia and Dr. Shaz Qadeer. His research focuses on designing tools and techniques in the area of programming languages, formal methods, and software engineering, and applying them to build reliable systems across domains like device drivers, distributed systems, robotics, and cyber-physical systems.
His research has had an impact both in Industry and Academia for which he was awarded the Sevin Rosen Funds Award for Innovation in 2018.
Before joining the graduate school, Ankush spent 2+ years at Microsoft Research (India) working with Dr. Sriram Rajamani and Dr. Shaz Qadeer applying formal methods to build reliable device drivers.
At IIT Kanpur, he was part of the team that built the first Indian Nano-Satellite JUGNU (launched on 12 October 2011). As a part of his Master's thesis, he designed and implemented the software stack for the on-board computer of the satellite.