I am Parasara Sridhar Duggirala, a third year PhD student in the Computer Science Department at University of Illinois at Urbana Champaign (UIUC). I am currently working with Prof. Mahesh Viswanathan and Prof. Sayan Mitra in the domain of Hybrid Systems, a formalism used to model Cyber-Physical Systems which interaction with the physical world and are controlled by software. My research is mainly about developing abstraction and approximation techniques for verification of such systems and make them scalable to large dimensional systems with complex software. I also have keen interest in Probabilistic Systems (like Discrete and Continuous Time Markov Chains and Markov Decision Processes) and their analysis. I also worked on monitoring and analyzing global predicates of Distributed Cyber-Physical Systems from sampled traces and static analysis. I frequently read papers in the general domain of Control Theory, Software Verification, Symbolic Execution, Testing Based Verification, Invariant Generation, Embedded and Real-Time Systems, SAT/SMT and Decision Procedures for Non-Linear Real Arithmetic.
Prior to joining UIUC, I pursued Undergraduate studies at Indian Institute of Technology Guwahati (IIT Guwahati) in Department of Computer Science and Engineering. While at IIT Guwahati, I worked with Prof. Hemangee Kapoor on Latency Insensitive Design for Multiple Clock Domain. In the past, I have pursued internships at SRI International in the Computer Science Laboratory during Summer 2012, at NEC Labs America in the System Analysis and Verification Group during Summer 2011 and at Verimag in the Timed and Hybrid Systems Group under the supervision of Dr. Oded Maler during Summer 2008.
Apart from Research
I am tech savvy and I follow WIRED, TechCrunch, Engadget, Slashdot, Linux.com and other interesting websites. Books written by Malcom Gladwell, Plato, Douglas Adams and Gurucharan Das have kindled my interest in Philosophy and Social Psychology. I am a science enthusiast and occasionally read papers from completely unrelated domain like Physics, Biology, Economics, etc. I am an admirer and have read several works of Swami Vivekananda. I love Telugu Literature (తెలుగు సాహిత్యం) and I enjoy reading works of SriSri and Mullapudi Venkataramana. To know more about my interests, visit my personal page.
S.Das, P.S.Duggirala, H.K.Kapoor, "A Formal Framework for Interfacing Mixed-Timing System", Integration, the VLSI journal. Published June 2013.
P.Prabhakar, P.S.Duggirala, S.Mitra, M.Viswanathan, "Hybrid Automata based CEGAR for Rectangular Hybrid Systems", Formal Methods in System Design (FMSD), (under review.)
Conference Publications (peer reviewed)
P.S.Duggirala, L. Wang, S.Mitra, M.Viswanathan, C. Munoz, "Temporal Precedence Checking for Switched Models and its Application to a Parallel Landing Protocol", International Symposium on Formal Methods (FM), May 2014. (Accepted for publication.)
P.S.Duggirala, S.Mitra, M.Viswanathan, "Verification of Annotated Models from Executions", International Conference on Embedded Software (EMSOFT), September 2013.
P.S.Duggirala, A.Tiwari, "Safety Verification for Linear Systems", International Conference on Embedded Software (EMSOFT), September 2013.
Best Paper Award.
P.Prabhakar, P.S.Duggirala, S.Mitra, M.Viswanathan, "Hybrid Automata Based CEGAR for Hybrid Systems", Verification Model Checking and Abstract Interpretation (VMCAI), January 2013.
P.S.Duggirala, T.T.Johnson, A.Zimmerman, S.Mitra, "Static and Dynamic Analysis of Timed Distributed Traces", IEEE Real-Time Systems Symposium (RTSS), December 2012.
K.Ghorbal, P.S.Duggirala, F.Ivancic, V.Kahlon, A.Gupta, "Efficient Probabilistic Model Checking of Systems with Ranged Probabilities", Reachability Problems (RP), September 2012.
P.S.Duggirala, S.Mitra, "Lyapunov Abstractions for Inevitability of Hybrid Systems", Hybrid Systems Computation and Control (HSCC), April 2012.
P.S.Duggirala, S.Mitra, "Abstraction Refinement for Stability", International Conference on Cyber-Physical Systems (ICCPS), April 2011.
P.S.Duggirala, S.Mitra, R.Kumar, D.Glazeski, "On the Theory of Stochastic Processors", Quantitative Evaluation of SysTems (QEST), September 2010.
Dynamic Analysis of Cyber-Physical Systems
Midwest Verification Day, September 2013
University of Illinois at Chicago, Chicago, Illinois.
Static and Dynamic Analysis of Timed Distributed Traces
Formal Methods Seminar, November 2012
Computer Science Department, Urbana, Illinois.
Introduction to Counterexample Guided Abstraction Refinement (CEGAR)
SRI International, Computer Science Laboratory, July 2012
Menlo Park, California.
Lyapunov Abstractions for Inevitability of Hybrid Systems
SRI International, Computer Science Laboratory, June 2012
Menlo Park, California.
Abstractions for Verification of Cyber-Physical Systems
60th CSL Anniversary Symposium, October 27-28, 2011
Coordinate Science Laboratory, Urbana, Illinois.
Abstraction Refinement for Stability
International Conference on Cyber-Physical Systems, April 12-14, 2011
Cyber-Physical Systems Week (CPS Week), Chicago, Illinois.
Stochastic Processors: Design, Analysis and Challenges
6th CSL Student Conference, January 27-28, 2011
Coordinate Science Laboratory, Urbana, Illinois.
Automatic Attack Generation for Firefox Extensions
NEC Labs America, January 6, 2011
Princeton, New Jersey.
On the Theory of Stochastic Processors
Quantitative Evaluation of SysTems (QEST) Conference, September 15-18, 2010
College of William & Mary, Williamsburg, Virginia.
Verification of Hybrid Systems
Hybrid systems are such systems which interact with the physical world and have both continuous dynamics and discrete switches. The continuous dynamics defines the evolutions of real valued variables and the discrete switches represent the change in the software state of the system. Hybrid Systems are commonly used as mathematical representation of Embedded Systems which interact with physical world. Verification of such systems involves challenges from two perspectives. Firstly, the complexity of the continuous dynamics makes the analysis of such systems difficult. As the number of dimensions in the system increases, analysis of continuous dynamics becomes increasingly challenging, this is called "curse of dimensionality". Secondly, because of the discrete changes in continuous dynamics, analysis coupling discrete changes and continuous evolution is difficult.
To achieve scalability of verification of Hybrid Systems, one could use several abstraction mechanisms for abstracting the continuous dynamics hence leading to simpler analysis of dynamics. To handle the discrete dynamics of such systems, SAT/SMT solvers and efficient decisions procedures can be employed. My research in the area of verification of Hybrid Systems would be to come up with decision procedures which could combine both abstraction techniques and SAT/SMT solvers.
If we extend these Hybrid Systems where different agents communicate over a network, it leads to Distributed Hybrid Systems. These are used to model the interactions of Distributed Cyber-Physical Systems where different nodes (controlled by software) interact with each other and perform a common action, such as fleet of robots or UAVs. My research in this area would be to develop monitors and use static and dynamic analysis over the executions of the system obtained.
I am interested in developing efficient algorithms for verification of properties of probabilistic systems modeled as Discrete Time Markov Chains (DTMCs). However, when these transition probabilities are not "exactly" known, but can be guaranteed to lie in an interval, such systems can be represented as Interval Discrete Time Markov Chains (IDTMCs). For efficient model checking of such systems, one could employ techniques like Interval Analysis and Affine Analysis and use off the shelf Linear Programing Solvers like GLPK or develop efficient algorithms based on the structure of linear constraints.
I am also interested in developing models for Stochastic Processors which describe the behavior of hardware with quantified uncertainties. Also, I am interested in developing and verifying new Randomized Distributed Algorithms which can be modeled as Markov Decision Processes (MDPs) which have both probabilities and non-determinism.
I am interested in testing approaches for software verification and also employ Constraint Solvers for generating automatic inputs. In the case of Firefox extensions, these inputs correspond to strings that can cause privilege escalation attacks as a result of the Firefox extensions. Such input strings can be generated from using the string constriant solvers like HAMPI and KUDZU.
Experience and Awards
SRI International, Menlo Park, California
NEC Labs America, Princeton, New Jersey
- Research Assistant,
University of Illinois Urbana Champaign, Illinois
Fall 2009 - present.
Verimag, Timed and Hybrid Systems Group, Grenoble,
Network Systems Laboratory, IIT Madras, India
Le Wang : Undergraduate in CE, University of Illinois Urbana Champaign.
Project : Verification of Parallel Aircraft Landing Protocol (ALAS) using C2E2.
Yi Lu :
Undergraduate in EE, University of Illinois Urbana
Project : Modeling and Analysis of Nonlinear Biological Systems.
- Held the position of SUN Campus Ambassador and earned monetary rewards for popularizing technologies of SUN Microsystems at IIT Guwahati.
- Awarded scholarship by EGIDE, French Republic, for internship at Verimag Laboratory for a period of 12 weeks.
- Lead a team of students develop and deploy the software for elections of Students' council at IIT Guwahati.
- Held the position of services secretary and technical coordinator for CSEA, a computer science students association at IIT Guwahati.
- Secured 99.95 percentile in the IIT Joint Entrance Examination, 2005 (among the 250,000 students).
- Secured Special Mention in Regional Mathematics Olympiad in the year 2004 for novelty in problem solving.
The best way to contact me is via e-mail. You can reach me at the following e-mail addresses.
To know more about my hobbies, please visit my personal page.