Prasad Sistla

Research Interests:

Formal methods in concurrent and distributed systems, semantics and verification of concurrent programs, database management systems

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. This project proposes various methods for static as well as runtime verification of such computer systems.

As part of the static verification, the project investigates model checking based methods for analysis and verification. It explores such methods for deterministic as well as probabilistic systems.

As part of the run time verification, project develops 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 are used for safe deployment and operation of Cyber Physical Systems such as Autonomous cars, Home assist robots, etc. The project employs Hidden Markov Models for capturing the behavior of such systems and develops accurate and timely monitors for detecting erroneous behavior in such systems.

• Emptiness under isolation and the Value problem for hierarchical probabilistic automata (with R. Chadha and M. Viswanathan), 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), April 22-29, 2017, Uppsala, Sweden.
• Decision Theoretic Monitoring of Cyber Physical Systems (with Andrey Yavolovsky and Milos Zefran), Proceedings of the 16th International Conference on Runtime Verification (RV2016), September 23-30 2016, Madrid, Spain.
• Distinguishing Hidden Markov Chains (with Stefan Kiefer), Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS2016), July 5-8,2016, New York City, USA.
• Model Checking Failure Prone Open Systems Using Probabilistic Automata (with Yue Ben), Proceedings of 13th International Symposium on Automated Technology for Verification and Analysis (ATVA2015), October 12-15,2015, Shanghai, China.
• Decidable and Expressive classes of Probabilistic Automata (with R. Chadha and M. Viswanathan), 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015), April 11-18, 2015, London, UK.
• Timely Monitoring in Partially Observable Stochastic Systems (with M. Zefran, Yao Feng and Yue Ben), 17th International Conference on Hybrid Systems: Computation and Control (HSCC 2014), April 15-17, 2014, Berlin, Germany.
• Probabilistic Automata with isolated cut points (with Rohit Chadha and Mahesh Viswanathan), 38th International Symposium Mathematical Foundations of Computer Science, August 2013, Klosterneuburg, Austria.
• Runtime Monitoring of Stochastic Cyber-Physical Systems with Hybrid State (with M. Zefran and Yao Feng),2nd International Conference on Runtime Verification (RV 2011), September 27 – September 30, 2011 San Francisco, California.
• Monitorability in Stochastic Dynamical Systems (with M. Zefran and Yao Feng), 23rd International Conference on Computer Aided Verifications, July 14-20, Cliff Lodge, Utah, 2011 (CAV 2011).
• Probabilistic Buchi Automata with Non-extremal Thresholds (with Rohit Chadha and Mahesh Viswanathan), 12th International Conference on Verification, Model checking and Abstract Interpretation, Austin, Texas, January 23-25, 2011 (VMCAI 2011).
• Model Checking Concurrent Programs with Nondeterminism and Randomization (with Rohit Chadha and Mahesh Viswanathan), 30th International Conference on Foundations of Software Technology and Theoretical Computer Science , Chennai, India, December 15-18, 2010 (FSTTCS 2010).
• Power of Randomization in Automata on Infinite Strings (with R. Chadha and M. Viswanathan), 20th International Conference on Concurrency Theory, Bologna, Italy, September 2009 (CONCUR 2009).
• Monitoring the Full range of Omega-regular properties of Stochastic Systems (with Kalpana Gondi and Yogesh Patel), Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI2009), Savannah, Georgia, 2009.
• Monitoring Temporal Properties of Stochastic Systems In Proceedings of International Conference on Verification, Model Checking and Abstract Interpretation. Lecture Notes in Computer Science, vol. 4905. Springer-Verlag, Berlin, Germany, 294-308, January 2008.
• On the Expressiveness and Complexity of Randomization in Finite State Monitors (with R. Chadha, M. Viswanathan), IEEE Symposium on Logic in Computer Science (LICS’08), Pittsburgh, June, 2008.
• Verification of Object-Relational Maps, (with K. Mehra, S. Rajamani and S. Jha), Fifth IEEE Symposium on Software Engineering and Formal Methods, London, September, 2007.
• Model checking Systems that employ Commutative Functions International Conf on Verification, ModelChecking and Abstract Interpretation, Paris, January 2005.
• Taming Interface Specifications Revised version of the papers that appeared in CONCUR 2005, August 2005.
• Checking Extended CTL Properties using Guarded Quotient Structures IEEE International Conference on Software Engineering and Formal Methods, Beijing, October, 2004.
• Symmetry and Reduced Symmetry in Model Checking , ACM Transactions on Programming Languages and Systems, Vol 26, Issue 2, July 2004, pp 702-734.
• SMC: A Symmetry Based Model-checker for Verification of Liveness Properties , ACM Transactions on Software Engineering Methodologies and Systems, July 2000.
• Using Symmetry When Model-checking under Fairness Assumptions: An Automata Theoretic Approach (with E. A. Emerson), ACM Transactions on Programming Languages and Systems, Vol. 19, No. 4, July 1997.
• Parameterized Verification of Linear Networks using Automata as Invariants (with V. Gyuris), Journal of Formal Aspects of Computing, Volume 11, Number 4 / December, 1999; Earlier version was presented at the 9th International Conference on Computer Aided Verification, Haifa, Israel, June 1997.
• On-the-Fly Model checking under Fairness that Exploits Symmetry (with V. Gyuris), Journal of Formal Methods in System Design,Volume 1254, 1997; Earlier version appeared in the International Conference on Computer Aided Verification, Haifa, Israel, June 1997.
• Symmetry and Model-checking (with E. A. Emerson), Formal Methods in System Design, 9(1/2), 1996, pp 105-130.
• Verification of a Real-life Protocol Using Symbolic Model-checking (with V. G. Naik), 6th International Conference on Computer Aided Verification, Stanford, California, June 1994; Also appeared in Springer-Verlag Lecture Notes in Computer Science.
• On Model-checking for the Mu-calculus and its fragments (with E. A. Emerson and C. S. Jutla), Journal of Theoretical Computer Science, 258(1-2): 491-522 (2001) (Preliminary version presented at the Fifth International Conference on Computer Aided Verification, Elounda, Crete, Greece June 28- July 1, 1993; Appeared in Lecture Notes in Computer Science 697, Springer-Verlag).

Security

Our projects in security are broadly focussed in two directions. The first direction is on exploring model checking based techniques for analyzing access control policies and for verifying security properties of programs. The second direction is towards developing program transformation techniques for preventing leakage of confidential information.

• DEICS: Data Erasure In Concurrent Software (with K. Gondi and V. N. Venkatakrishnan), The 19th Nordic Conference on Secure IT Systems (NordSec 2014),Tromso,Norway, October 15-17, 2014.
• WEBLOG:A Declarative Language for Secure Web Development (with T. Hinrichs, D. Rosetti, G. Petronella, V. Venkatakrishnan and L. Zuck), ACM SIGPLAN Eighth Workshop on Programming Languages and Analysis for Security (PLAS), June 2013, Seattle, Washington.
• SWIPE: Eager Erasure of Sensitive Data in Large scale Systems Software (with K. Gondi, P. Bisht, P. Venkatachari and V. N. Venkatakrishnan),Second ACM Conference on Data and Application Security and Privacy (CODASPY 012), pp 295-306, Feb 7-9, 2012, San Antonio, TX.
• TAPS: Automatically Preparing Safe SQL Queries (with Prithvi Bisht and V.N. Venkatakrishnan), ACM Conference on Computer and Communication Security 2010 (CCS’2010), October, Chicago, Illinois (Demo paper).
• Automatically Preparing Safe SQL Queries (with Prithvi Bisht and V.N. Venkatakrishnan), Fourteenth International Conference on Financial Cryptography and Data Security’10, Tenerife, Canary Islands, Spain, January 2010.
• CMV: Automatic Verification of Complete Mediation for Java Virtual Machines (with V. N. Venkatakrishnan, M. Zhou, H. Branske),ACM Symposium on Information, Computer and Communication Security (ASIACCS’08), Tokyo 18-20 March 2008.
• Preventing Information Leaks Through Shadow executions (with R. Capizzi, A. Longo and V. N. Venkatakrishnan), Annual Computer Security Applications Conference (ACSAC 2008), Annaheim, California, December 2008.
• Analysis of Dynamic Policies (with Min Zhou) FCS-ARSPA’06, Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, Seattle, August 15-16, 2006.
  • Analysis of Dynamic Policies (with M. Zhou), Information and Computation, Vol. 206/2-4, pp 185-212.
• Language based Policy Analysis in a SPKI Trust Management System (with Arun Eamani) Fourth PKI Annual R&D Workshop: Multiple Paths to Trust, NIST Gaithersburg, Maryland, April 2005.
  • Language based Policy Analysis in SPKI Trust Management Systems (with A. Eamani),Journal of Computer Security Volume 14, Number 4(2006), pp 327-357.

Database Management Systems

• Polarity Consistency Checking for Sentiment Dictionaries (with with Eduard Dragut, Hong Wang, Clement Yu, Weiyi Meng), ACL 2012 : The 50th Annual Meeting of the Association for Computational Linguistics, July 8-Jul 12, 2012, Jeju, Korea.
• Answer-Pairs and Processing of Continuous Nearest-Neighbor Queries (with Ouri Wolfson and Bo Xu),The Seventh ACM SIGACT/SIGMOBILE International Workshop on Foundations of Mobile Computing (FOMC2011), June 2011, SanJose, California.
• Construction of a Sentimental Word Dictionary (with Eduardo Draghut, Weiyi Meng and Clement Yu), 19th ACM International Conference on Information and Knowledge Management (CIKM 2010), Toronto, Canada, October 26-30, 2010.
• Stop Word and Related Problems in Web Interface Integration (with Eduardo Draghut, Fang Fang, Clement Yu and Weiyi Meng), 35th International Conference on Very Large Database Systems, Lyon, France, August 2009 (VLDB 2009).
• A data model for trip planning in multimodal transportation systems (with Joel Booth, Ouri Wolfson and Isabel Cruz), 12th International Conference on Extended Databased Technology (EDBT 2009), March 2009, St Petersburg, Russia.
• A Query Processor for Prediction based Monitoring of Data Streams (with Sergio Illari, Ouri Wolfson, Eduardo Mena and Arantza Illarramendi) 12th International Conference on Extended Databased Technology (EDBT 2009), March 2009, St Petersburg, Russia.
• Similarity Based Retrieval of Videos (with C. Yu et al), Proc. 13th International Conference on Data Engineering (ICDE), 1997.
• Retrieval of Pictures Using Approximate Matching (with C. Yu et al), Multi-Media Databases Systems, edited by V. Subramanian and S. Jajodia, 1996.
• Similarity Based Retrieval of Pictures Using Indices on Spatial Relationships (with C. Yu et al), Proc. 21st International Conference on Very Large Database Systems (VLDB), 1995.The other project in databases is on cost models in digital libraries, and on active and mobile databases, similarity based retrieval from sequence databases.
• Formal Languages and Algorithms for Similarity Based Retrieval from Sequence Databases , 22nd International Conf on Foundations of Software Technology and Theoretical Computer Science, Kanpur, India, Springer-Verlag Lecture Notes in Computer Science 2556, Dec. 2002.
• Similarity based Retrievl from Sequence Databases using Automata as Queries” (with Tao Hu and V. Chowdhry), Proc. 11th International Conference on Knowledge and Information Management (CIKM), Nov 2002. Also Technical Report, Dept of EECS, University of Illinois at Chicago, 2000
• Towards a Theory of Cost Management in Digital Libraries and Electronic Commerce (with O. Wolfson et al), ACM Transactions on Database Systems, 1998.
• Modeling and Querying Moving Objects (with O. wolfson, S. Chamberlin et al), Proc. 13th International Conference on Data Engineering (ICDE), 1997

Harvard University, Cambridge, Massachusetts: Ph.D. Computer Science/Applied Mathematics, 1983
Indian Institute of Science, Bangalore, India: M.E. Computer Science, 1976
B.Tech., Electronics and Communications Engineering, 1974