Aravinda Prasad Sistla
Professor
Department of Computer Science
Contact
Building & Room:
1100 SEO
Address:
851 S. Morgan St, MC 152, Chicago, IL, 60607
Office Phone:
Email:
Related Sites:
About
I am interested in the following areas of research:
Formal Methods in Concurrent and Distributed Systems
With the widespread use of distributed and concurrent systems and with the increase in the complexity of software for such systems, it becomes important to develop various methods for ensuring the quality of concurrent software systems. I am interested in various methods for static as well as runtime verification of such computer systems.
As part of the static verification, I am interested model checking based methods for analysis and verification of deterministic as well as probabilistic systems. My early works in this area included the earliest work that gave a linear time model checking algorithm that checks whether the reachability graph of a concurrent program, given as a Kripke structure, satisfies a property specified in the branching time temporal logic CTL. These works also included results on the complexity of model checking and satisfiability checking for specifications given in Linear Temporal Logic, LTL. They also gave methods that employ symmetry reductions for ameliorating the state explosion problem in explicit state model checking algorithms. The later results were implemented in Symmetry based Model Checker (SMC) for checking safety and liveness properties. I also gave the earliest decidability result on model checking parameterized system of processes, i.e., checking if a system of processes composed of an arbitrary number of processes, satisfies a property specified in LTL.
As part of the run time verification, I am interested in methods for detecting faults at execution time when the faults are specified on the underlying computations of the system in expressive languages such as temporal logic and automata. The developed methods can be used for run time verification of partially observable stochastic systems. An application of these methods is for safe deployment and operation of Cyber Physical Systems such as Autonomous cars, Home assist robots, etc. These methods employ Hidden Markov Models for capturing the behavior of such systems and develop accurate and timely monitors for detecting erroneous behavior in such systems.
Security
My interests in security are broadly focussed in two directions. The first direction is on exploring model checking based techniques for analyzing access control policies, for verifying randomized security/cryptographic protocols and for verifying privacy claims of differential privacy mechanisms. The second direction is towards developing program transformation techniques for preventing leakage of confidential information.
Database Management Systems
My earlier work in database systems include work on specification and processing of queries in moving object databases, active databases and textual databases. My current interests continue to be in these sub-areas of database management systems.
List of Publications
List of my publications can be obtained using the link dblp , or the link Google Scholar Profile or my vitae c.v..
Education
Harvard University, Cambridge, Massachusetts: Ph.D. Computer Science/Applied Mathematics, 1983
Indian Institute of Science, Bangalore, India: M.E. Computer Science, 1976
National Institute of Technology, Warangal, India, B.Tech., Electronics and Communications Engineering, 1974