The increasing demand for automation in safety-critical applications such as aeronautics, automotive, industrial process control, medical devices and so on, has pressurized the need for scalable formal analysis techniques for ensuring reliable and error-free operation of the systems. A unique feature of these systems is the mixed discrete continuous behaviors they exhibit, which is due to the interaction between a digital computer controlling and a physical entity. From the point of view of computability, presence of the continuous dynamics makes the problem challenging so much so that the verification of even simple properties becomes un-decidable for a class of systems with fairly simple continuous dynamics. Approximations have proven to be a key component in dealing with the state space explosion resulting from the hybrid models. In this talk, we will discuss various approximation techniques for different classes of systems and properties, including, counter-example guided abstraction refinement and bounded error-approximations.
Pavithra Prabhakar is currently a CMI postdoctoral fellow at the California Institute of Technology with a joint appointment at the IMDEA Software Institute in Madrid. She obtained her PhD in Computer Science from the University of Illinois at Urbana-Champaign in 2011, where she was a member of the Formal Methods group. She received her BTech from the National Institute of Technology, Warangal in 2004 and MS from the Indian Institute of Science, Bangalore in 2006, both in Computer Science. She also has a master’s degree in Applied Mathematics from the University of Illinois at Urbana-Champaign. She was an intern at Bell Labs, Alcatel-Lucent, NJ during the summers of 2009 and 2010, and a Visiting student at the Laboratoire Specification et Verification, ENS de Cachan In Spring 2006. She is a recipient of the Sohaib and Sara Abbasi Fellowship from the department of computer science at the University of Illinois at Urbana-Champaign and the Dr MNS Swamy medal from the department of computer science and automation at the Indian Institute of Science for the best master’s thesis. Her research focuses on developing formal techniques for the design, verification and analysis of timed and hybrid systems. Recent emphasis has been on studying approximation methods for the algorithmic verification of safety and stability properties of hybrid systems.