Publications

Journals

[13] Rohit Chadha, Vincent Cheval, Stefan Ciobaca, and Steve Kremer. Automated Verification of Equivalence Properties of Cryptographic Protocols. ACM Transactions on Computational Logic , 17(4):23, 2016. [ bib | .pdf ]
[12] Rohit Chadha, Mahesh Viswanathan, and Ramesh Viswanathan. Least upper bounds for probability measures and their applications to abstractions. Information and Computation, 234:68–106, 2014. [ bib | .pdf ]
[11] Rémi Bonnet, Rohit Chadha, P. Madhusudan, and Mahesh Viswanathan. Reachability under contextual locking. Logical Methods in Computer Science, 9(3), 2013. [ bib | .pdf ]
[10] Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Power of randomization in automata on infinite strings. Logical Methods in Computer Science, 7(3), 2011. [ bib  | .pdf ]
[9] Rohit Chadha and Mahesh Viswanathan. A counterexample guided abstraction-refinement framework for Markov Decision Processes. ACM Transactions on Computational Logic, 12(1):1–49, 2010. [ bib  | .pdf ]
[8] Rohit Chadha and Mahesh Viswanathan. Deciding branching-time properties for asynchronous programs. Theoretical Computer Science, 410(42):4169–4179, 2009. [ bib  | .pdf ]
[7] Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. On the expressiveness and complexity of randomization in finite state monitors. Journal of the ACM, 56(5), 2009. [ bib  | .pdf ]
[6] Pedro Baltazar, Rohit Chadha, and Paulo Mateus. Quantum computation tree logic — model checking and complete calculus. International Journal of Quantum Information, 6(2):281–302, 2008. [ bib ]
[5] Rohit Chadha, Luis Cruz-Filipe, Paulo Mateus, and Amilcar Sernadas. Reasoning about probabilistic sequential programs. Theoretical Computer Science, 379(1):142–165, 2007. [ bib ]
[4] Rohit Chadha, Paulo Mateus, and Amilcar Sernadas. Reasoning about imperative quantum programs. Electronic Notes in Theoretical Computer Science, 158:19–39, 2006. [ bib ]
[3] Rohit Chadha, Damiano Macedonio, and Vladimiro Sassone. A hybrid intuitionistic logic: Semantics and decidability. Journal of Logic and Computation (Special issue on Logics for Resources, Processes and Programs, 16(1):27–59, 2006. [ bib ]
[2] Rohit Chadha, Steve Kremer, and Andre Scedrov. Formal analysis of multiparty contract signing. Journal of Automated Reasoning, 36(1):39–83, 2006. [ bib ]
[1] Rohit Chadha, John Mitchell, Andre Scedrov, and Vitaly Shmatikov. Contract signing, optimism and advantage. Journal of Logic and Algebraic Programming (Special issue on Modeling and Verification of Cryptographic Protocols), 64(2):189–218, 2005. [ bib  | .pdf ]

Conference Articles

[28] Matt Bauer, Rohit Chadha and Mahesh Viswanathan. Modular Verification of Protocol Equivalence in the Presence of Randomness. In Dieter Gollman and Simon Foley, editors, 22nd European Symposium on Research in Computer Security (ESORICS), 2017. pages 187–205, 2017. [ bib | .pdf ]
[27] Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan. Verification of randomized security protocols. In Joel Oukanine, editor, Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2017. pages 1–12, 2017. [ bib | .pdf ]
[26] Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan. Emptiness under isolation and the value problem for hierarchical probabilistic automata. In Javier Esparza and Andrzej Murawski, editors, 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS),  pages 231–247, 2017.  [ bib | .pdf ]
[25] Matt Bauer, Rohit Chadha, and Mahesh Viswanathan. Composing protocols with randomized actions. In Frank Piessens and Luca Viganò, editors, 5th Conference on Principles of Security and Trust (POST 2016), pages 189–210, 2016. [ bib | .pdf ]
[24] Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan, and Yue Ben. Decidable and expressive classes of probabilistic automata. In Andrew Pitts, editor, 16th International Conference on Foundations of Software Science and Computation Structures, pages 200–214, 2015. [ bib | .pdf ]
[23] Rohit Chadha, Umang Mathur, and Stefan Schwoon. Computing information leakage using symbolic model-checking. In Venkatesh Raman and S. P. Suresh, editors, Annual Conference on Foundations of Software Technology and Theoretical Computer Science, pages 505–516, 2014. [ bib | .pdf ]
[22] Rohit Chadha, Dilip Kini, and Mahesh Viswanathan. Decidable problems for unary pfas. In Gethin Norman and William H. Sanders, editors, 11th International Conference on Quantitative Evaluation of Systems, pages 329–344, 2014. [ bib | .pdf ]
[21] Rohit Chadha, Dileep Kini, and Mahesh Viswanathan. Quantitative information flow in Boolean programs. In 3rd Conference on Principles of Security and Trust, pages 103–119, 2014. [ bib | .pdf ]
[20] Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Probabilistic automata with isolated cut-points. In K. Chatterjee and J. Sgall, editors, 38th International Symposium on Mathematical Foundations of Computer Science, pages 254–265, 2013. [ bib | .pdf ]
[19] Rémi Bonnet and Rohit Chadha. Bounded context-switching and reentrant locking. In Frank Pfenning, editor, 16th International Conference on Foundations of Software Science and Computation Structures, volume 7794 of Lecture Notes in Computer Science, pages 65–80, 2013. [ bib | .pdf ]
[18] Rohit Chadha, Stefan Ciobaca, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. In Helmut Seidl, editor, 22nd European Symposium on Programming (ESOP ’12), volume 7211 of Lecture Notes in Computer Science, pages 108–127, 2012. [ bib | .pdf ]
[17] Rohit Chadha and Michael Ummels. The complexity of information leakage in recursive programs. In Deepak D’Souza, T. Kavitha, and Jaikumar Radhakrishnan, editors, 32nd Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS ’12), pages 534–545, 2012. [ bib | .pdf ]
[16] Rohit Chadha, P. Madhusudan, and M. Viswanathan. Reachability under contextual locking. In Cormac Flanagan and Barbara König, editors, 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’12, pages 437–450. Springer, 2012. [ bib | .pdf]
[15] Rohit Chadha, Vijay Korthikranthi, Mahesh Viswanathan, Gul Agha, and Youngmin Kwon. Model checking mdps with a unique compact invariant set of distributions. In Alma Riska and Catuscia Palamidessi, editors, Eighth International Conference on Quantitative Evaluation of SysTems (QEST ’11), pages 121–130. IEEE Computer Society, 2011. [ bib  | .pdf ]
[14] Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Probablistic Büchi automata with non-extremal acceptance thresholds. In Ranjit Jhala and David A. Schmidt, editors, Twelfth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI ’11), pages 103–117, 2011. [ bib  | .pdf ]
[13] Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Model checking concurrent programs with nondeterminism and randomization. In Kamal Lodaya and Meena Mahajan, editors, Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS ’10), pages 364–375, 2010. [ bib  | .pdf ]
[12] Rohit Chadha, Axel Legay, Pavithra Prabhakar, and Mahesh Viswanathan. Complexity bounds for the verification of real-time software. In Gilles Barthe and Manuel Hermenegildo, editors, Proceedings of the 11th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI ’10), volume 5944 of Lecture Notes in Computer Science, pages 95–111, 2010. [ bib ]
[11] Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Power of randomization in automata on infinite strings. In Mario Bravetti and Gianluigi Zavattaro, editors, Proceedings of the 20th International Conference on Concurrency Theory (CONCUR ’09), volume 5710 of Lecture Notes in Computer Science, pages 229–243, 2009. [ bib ]
[10] Rohit Chadha, Stéphanie Delaune, and Steve Kremer. Epistemic logic for the applied pi calculus. In David Lee, Antónia Lopes, and Arnd Poetzsch-Heffter, editors, Proceedings of IFIP International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE ’09), volume 5522 of Lecture Notes in Computer Science, pages 182–197, 2009. [ bib  | .pdf ]
[9] Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. On the expressiveness and complexity of randomization in finite state monitors. In 23rd Annual IEEE Symposium on Logic in Computer Science (LICS ’08), pages 18–29, 2008. [ bib ]
[8] Rohit Chadha, Carl A. Gunter, Jose Meseguer, Ravinder Shankesi, and Mahesh Viswanathan. Modular preservation of safety properties by cookie-based dos-protection wrappers. In Gilles Barthe and Frank S. de Boer, editors, 10th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS ’10), volume 5051, pages 39–58. Springer, 2008. [ bib ]
[7] Rohit Chadha and Mahesh Viswanathan. Decidability results for well-structured transition systems with auxiliary storage. In Luís Caires and Vasco Thudichum Vasconcelos, editors, 18th International Conference on Concurrency Theory (CONCUR ’07), volume 4703 of Lecture Notes in Computer Science, pages 136–150. Springer, 2007. [ bib  | .pdf ]
[6] Pedro Baltazar, Rohit Chadha, Paulo Mateus, and Amílcar Sernadas. Towards model-checking quantum security protocols. In First International Conference on Quantum, Nano, and Micro Technologies (ICQNM’ 2007), page 14. IEEE Computer Society, 2007. [ bib ]
[5] Rohit Chadha, Paulo Mateus, and Amilcar Sernadas. Reasoning about states of probabilistic sequential programs. In Zoltán Ésik, editor, Computer Science Logic, 20th International Workshop (CSL ’06), volume 4207 of Lecture Notes in Computer Science, pages 240–255. Spinger, 2006. [ bib ]
[4] Rohit Chadha, Steve Kremer, and Andre Scedrov. Formal analysis of multi-party contract signing. In R. Focardi, editor, 17th IEEE Computer Security Foundations Workshop (CSFW ’04), pages 266–279. IEEE Computer Society, 2004. [ bib ]
[3] Rohit Chadha, John Mitchell, Andre Scedrov, and Vitaly Shmatikov. Contract signing, optimism and advantage. In R. Amadio and D. Lugiez, editors, 14th International Conference on Concurrency Theory (CONCUR ’03), pages 366–382. Springer-Verlag, 2003. [ bib ]
[2] Rohit Chadha, Max Kanovich, and Andre Scedrov. Inductive methods and contract-signing protocols. In P. Samarati, editor, 8th ACM Conference on Computer and Communications Security (CCS ’01), pages 176–185. ACM Press, 2001. [ bib ]
[1] Rohit Chadha, Mahesh Viswanathan, and Ramesh Viswanathan. Least upper bounds for probability measures and their applications to abstractions. In Franck van Breugel and Marsha Chechik, editors, 19th International Conference on Concurrency Theory (CONCUR ’08), volume 5201 of Lecture Notes in Computer Science, pages 264–278. Springer, 2008. [ bib ]