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).