Parasara Sridhar Duggirala
CS @ UIUC Homepage.
Research AreasMy current research interests include:
- Formal Methods
- Verification of Hybrid and Probabilistic Systems
- Software Verification
interested in developing
abstraction refinement mechanisms to improve the scalability of
Hybrid Systems. One of my recent projects is on infinite state
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
for proving termination (Terminator
Project by Microsoft Research) of
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.
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
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.
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.
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.
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.)