Parasara Sridhar Duggirala
CS @ UIUC Homepage.
Research Areas
My current research interests include:- Formal Methods
- Verification of Hybrid and Probabilistic Systems
- Software Verification
- Formal
Methods
and
Security
Hybrid Systems
I am
interested in developing
abstraction refinement mechanisms to improve the scalability of
verification of
Hybrid Systems. One of my recent projects is on infinite state
abstractions of
Hybrid Systems, which helps in reuse of existing tools for
verification. I have
also worked on proving stability of Hybrid Systems by using abstraction
refinement. This work is based on the ideas from software verification
domain
for proving termination (Terminator
Project by Microsoft Research) of
programs
and using abstraction refinement for the same. Further, these approaches were fused with ideas from Control Theory like
Lyapunov Functions. The fusion of these approaches provides us with better abstractions to prove liveness properties.
Publications
Parasara Sridhar Duggirala, Sayan Mitra. Lyapunov Abstractions for Inevitability of Hybrid Systems. Hybrid Systems Computation and Control (HSCC) 2011. (To Appear.)
Parasara Sridhar Duggirala, Sayan Mitra. Abstraction-Refinement for Stability. International Conference on Cyber-Physical Systems (ICCPS) 2011.
Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan. Hybrid Automata Based CEGAR for Hybrid Systems. (In Preperation.)
Software Verification, Formal Methods and Security
I have developed keen interest in formal methods and security. I am interested in applying techniques from Program Analysis (static and dynamic) and approaches from Model Checking for proving security. I am currently working on automatic attack input generation for Firefox browser extensions. The extensions for Firefox web-browser are completely written in JavaScript and to generate attacks on these extensions, static analysis is performed first. Further, the constraints obtained from static analysis are solved by using string constraint solvers.
Publications
Sruthi Bandhakavi, Parasara Sridhar Duggirala, Stanley Bak, Madhusudan Parthasarathy. Attack Input generation for Browser Extensions using String-Constraint Solvers. (Manuscript.)
Probabilistic Model Checking
I am interested in applying probabilistic model checking techniques for proving quantitative properties of systems. I have developed Discrete Time Markov Chain (DTMC) models for a new type of circuits called Stochastic Circuits, where the output is delayed based on delay distribution. Performance analysis of these circuits is done by Model Checking the correspoding DTMC models.
I have also worked on developing efficient algorithms for model checking systems with ranged probabilities. The traditional approaches for verifying bounded PCTL properties for Discrete Time Markov Chains (DTMCs) have been extended. In order to make the process efficient, approaches from Linear Programing, Affine Arithmetic and Interval Arithmetic are used.
Publications
Parasara Sridhar Duggirala, Khalil Ghorbal, Franjo Ivancic, Vineet Kahlon, Aarti Gupta. Efficient Model Checking of Systems with Ranged Probabilities. (In Preperation.)
Parasara Sridhar Duggirala, Sayan Mitra, Rakesh Kumar, Dean Glazeski. On The Theory Of Stochastic Processors. Quantitative Evaluation of SysTems (QEST) 2010.
Undergraduate Thesis
As a part of my undergraduate thesis, I have worked on Latency Insensitive (LI) Methodology for System on Chip design. Existing LI design is only applicable for single clock domains and I have worked on extending the LI design to multiple clock domains.
Publications
Parasara Sridhar Duggirala, Hemangee Kapoor, Shirshendu Das. Extending the Theory of Latency Insensitive Design to Multiple Clocks. IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC) 2011. (Under Review.)