Events Calendar

CS Colloquium: Jyotirmoy V. Deshmukh (Toyota Technical Center) -Ninja Temporal Logic: Making formal methods relevant in engineering practice

Speaker: Jyotirmoy V. Deshmukh, Toyota Technical Center

Talk Title: Ninja Temporal Logic: Making formal methods relevant in engineering practice

Series: CS Colloquium

Abstract: This lecture satisfies requirements for CSCI 591: Computer Science Research Colloquium.

The software that controls the operation of critical systems such as vehicles, medical devices, buildings, and transportation infrastructures is getting smarter due to the increased demands for autonomy. The push for increased automation is a worthy goal, but can we do so without compromising the safety and reliability of such systems?
Furthermore, can formal methods truly improve a design engineer's productivity? In this talk, I will introduce some of the most important questions facing academic and industrial development of software for the cyber-physical systems of tomorrow. We will consider solutions based on the use of formal logics, that, on one hand allow rigorous reasoning about system designs, while on the other, do not place an undue burden on the engineer. In particular, I will explain how formal requirements using real-time temporal logics have had an impact in the development of cutting-edge alternate-energy vehicles and advanced control problems within Toyota. I will guide the audience through an ecosystem built around temporal logic that permits automatic testing, efficient monitoring, requirement engineering and controller synthesis for highly complex automotive systems. The talk covers topics from what I consider the trifecta for designing reliable cyber-physical systems: formal logic, machine learning, and control theory, and will lay out my vision for future research and open problems within this domain.

Biography: Jyotirmoy V. Deshmukh is a Principal Engineer at Toyota R&D. He received his Ph.D. from the University of Texas at Austin under the supervision of E. Allen Emerson on topics including tree automata, verifying data structure libraries, static analysis for concurrent programs and program repair. He worked as a post-doctoral researcher at the University of Pennsylvania with Rajeev Alur's research group, investigating theoretical models of streaming computation and program synthesis techniques. For the last five years at Toyota, Jyo's research has focused on the design and analysis of industrial cyber-physical systems. Drawing on areas such as hybrid systems, real-time temporal logics, control theory, machine learning and dynamical systems theory, Jyo has been attempting to bridge the gap between academic research and its applicability to industrial-scale systems.

Host: CS Department

Location: Henry Salvatori Computer Science Center (SAL) - 101

Audiences: Everyone Is Invited

Contact: Assistant to CS chair