Publications

Dissertation

1. A formal analysis of exchange of digital signatures. Rohit Chadha. University of Pennsylvania. 2003. [pdf]

Book Chapters

1. Matt Bauer, Rohit Chadha, Mahesh Viswanathan. (2020) Modelchecking Safety Properties in Randomized Security Protocols. In V. Nigam, T. Ban Kirigin, C. Talcott, J. Guttman, S. Kuznetsov, B. Thau Loo and M. Okada, editors, editors, Logic, Language, and Security: Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday. Lecture Notes in Computer Science, vol 12300. pages 167-183, 2020. [pdf]

2. Rohit Chadha, Paulo Mateus, Amilcar Sernadas, and Cristina Sernadas. Extending classical logic for reasoning about quantum systems. In D. Gabbay K. Engesser and D. Lehmann, editors, Handbook of Quantum Logic and Quantum Structures: Quantum Logic, pages 325–372. Elsevier, 2009. [pdf]

Journal Publications

1. Kandasamy Muniasamy, Rohit Chadha, Prasad Calyam, M. Sethumadhavan. Analyzing Component Composability of Cloud Security Configurations. IEEE Access 11: 139935--13995, 17 pages, 2023. [Link]

2. Umang Mathur, Matthew S. Bauer, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan: Exact quantitative probabilistic model checking through rational search. Formal Methods Syst. Des. 56(1): 90-126 (2020). [pdf]

3. Gergei Bana, Rohit Chadha, Ajay K. Eeralla and M. Okada. Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability. ACM Transactions on Computational Logic. 21(1):2:1-2:44, 2020. [pdf]

4. Yue Ben, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan. Decidable and Expressive Classes of Probabilistic Automata. Journal of Computer and System Sciences. 100:70–95, 2019. [pdf]

5. 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:1–23:32, 2016. 32 pages+50 page electronic index. 5-year Impact factor: 1.159. Selected by ACM/ThinkLoud Computing Reviews as part of the 21st Annual Best of Computing list of Notable Books and Articles of 2016. [pdf]

6. 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. 39 pages. [pdf]

7. Remi Bonnet, Rohit Chadha, P. Madhusudan and Mahesh Viswanathan. Reachability under Contextual Locking. Logical Methods in Computer Science. (Special issue on Best Theoretical Papers of TACAS 2012). 9(3), 2013. 17 pages. [pdf]

8. Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Power of randomization in automata on infinite strings. Logical Methods in Computer Science. 7(3): 2011. 32 pages. [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. 49 pages. [pdf]

10. Rohit Chadha and Mahesh Viswanathan. Deciding branching-time properties for asynchronous programs. Theoretical Computer Science, 410(42):4169–4179, 2009. 11 pages. [pdf] 

11. 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): 26:1-26:44, 2009. 44 pages. [pdf]

12. 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. 22 pages. [pdf]

13. Rohit Chadha, Luis Cruz-Filipe, Paulo Mateus, and Amilcar Sernadas. Reasoning about probabilistic sequential programs. Theoretical Computer Science, 379(1-2):142–165, 2007. 26 pages. [pdf]

14. Rohit Chadha, Paulo Mateus, and Amilcar Sernadas. Reasoning about imperative quantum programs. Electronic Notes in Theoretical Computer Science, 158:19–39, 2006. 21 pages. Special Session on Quantum Computing at the Twenty-second Conference on the Mathematical Foundations of Programming Semantics, 2006, Genova. [pdf]

15. Rohit Chadha, Damiano Macedonio, and Vladimiro Sassone. A hybrid intuitionistic logic: Semantics and decidability. International Journal of Logic and Computation (Special issue on Logics for Resources, Processes and Programs), 16(1):27–59, 2006. 33 pages. [pdf]

16. Rohit Chadha, Steve Kremer, and Andre Scedrov. Formal analysis of multiparty contract signing. Journal of Automated Reasoning, 36(1-2):39–83, 2006. 45 pages. [pdf]

17. 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. 30 pages. Invited submission. [pdf]

Refereed Conference Publications

1. Cody Rivera, Bishnu Bhusal, Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan. Checking ∂-Satisfiability of Reals with Integrals. In Object-Oriented Programming, Systems, Languages & Applications (OOPSLA), 2025. Accepted. 

2. Nabarun Deka, Minjian Zhang, Rohit Chadha, Mahesh Viswanathan. Deciding Branching Hyperproperties for Real-Time Systems. In Toby 37th IEEE Computer Security Foundations Symposium (CSF), 2024, pages 65--79. Distinguished Paper Award. [pdf]

3. Saketh Poduvu, Roshan Lal Neupane, Alicia Esquivel Morel, Reshmi Mitra, Vijay Anand, Rohit Chadha, Prasad Calyam. Task-Based Access Control for Computation and Communication in the Tactical Warfighting Edge. In 2024 IEEE Military Communications Conference (MILCOM), 2024, pages 839--846. [Link]

4. Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan, Bishnu Bhusal. Deciding Differential Privacy of Online Algorithms with Multiple Variables. In 30th ACM SIGSAC Conference on Computer and  Communications Security, (CCS) 2023, pages 1761-1775. [pdf]

5. Ali Bajwa, Mingjian Zhang, Rohit Chadha, Mahesh Viswanathan. Stack-Aware Hyperproperties. In 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2023, pages 308--325. [pdf]

6. Vijay Anand, Natalie A. Bolton, Prasad Calyam, Rohit Chadha, Rajendra K. Raj, Sumita Mishra. Enhancing Computing Curricular Outcomes and Student Accomplishments Through Collegiate Competitions. In Venkatesh Choppella, Deepak B. Phatak and ACM Conference on Global Computing Education (CompEd), Vol 1, 2023, pages 22--28. [Link]

7. Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan. On Linear Time Decidability of Differential Privacy for Programs with Unbounded Inputs. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2021, pages 1--13. [pdf]

8. Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan. Deciding Accuracy of Differential Privacy Schemes. In 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), Vol 5:pages 1-30, 2021. [pdf]

9. Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan. Deciding Differential Privacy for Programs with Finite Inputs and Outputs. 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 141-154, 2020. [pdf]

10. Thomas N. Reynolds, William L. Harrison, Rohit Chadha, Gerard Allwein. Strongly bounded termination with applications to security and hardware synthesis. Proceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven Development, pages 1-10, 2020. [pdf]

11. Gergei Bana, Rohit Chadha and Ajay Kumar Eeralla. Formal Analysis of Vote Privacy Using Computationally Complete Symbolic Attacker. In 23rd European Symposium on Research in Computer Security (ESORICS), pages 350–372, 2018. [pdf]

12. Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan. Approximating Probabilistic Automata by Regular Languages. In 27th EACSL Annual Conference on Computer Science Logic (CSL), pages 14:1–14:23, 2018. [pdf]

13. Matt Bauer, Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan. Model Checking Indistinguishability of Randomized Security Protocols. In 30th International Conference on Computer-Aided Verification (CAV), pages 117–135, 2018. [pdf]

14. Matt Bauer, Umang Mathur, Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan. Exact Quantitative Model Checking Through Rational Search. In 17th International conference on Formal Methods in Computer-Aided Design (FMCAD), pages 92–99, 2017. [pdf]

15. Matt Bauer, Rohit Chadha and Mahesh Viswanathan. Modular Verification of Protocol Equivalence in the Presence of Randomness. In 22nd European Symposium on Research in Computer Security (ESORICS), pages 1–12, 2017. [pdf]

16. Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan. Verification of randomized security protocols. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pages 1–12, 2017. [pdf]

17. Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan. Emptiness under isolation and the value problem for hierarchical probabilistic automata. In 20th International Conference on Foundations of Software Science and Computation Structures, (FoSSaCS), pages 231–247, 2017. [pdf]

18. Matt Bauer, Rohit Chadha and Mahesh Viswanathan. Composing protocols with randomized actions. In 5th International Conference on Principles of Security and Trust (POST). Pages 189-210, 2016. [pdf]

19. Rohit Chadha, Mahesh Viswanathan, Prasad Sistla and Yue Ben. Decidable and Expressive classes of Probabilistic Automata. In 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), pages 200-214, 2015. [pdf]

20. Rohit Chadha, Umang Mathur and Stefan Schwoon. Computing information leakage using symbolic model-checking. In Annual Conference on Foundations of Software Technology and Theoretical Computer Science, (FST&TCS), pages 505-516, 2014. [pdf]

21. Rohit Chadha, Dilip Kini and Mahesh Viswanathan. Decidable problems for unary PFAs. In 11th International Conference on Quantitative Evaluation of Systems (QEST), pages 329–344, 2014. [pdf]

22. Rohit Chadha, Dileep Kini and Mahesh Viswanathan. Quantitative information flow in Boolean Programs. In 3rd International Conference on Principles of Security and Trust (POST), pages 103-119, 2014. [pdf]

23. Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan. Probabilistic Automata with Isolated Cut-Points. In 38th International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 8087 of Lecture Notes in Computer Science, pages 254-265, 2013. Springer. [pdf]

24. Remi Bonnet and Rohit Chadha. Bounded Context-Switching and Reentrant Locking. In 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), volume 7794 of Lecture Notes in Computer Science, pages 65-80, 2013. Springer. [pdf]

25. Rohit Chadha and Michael Ummels. The complexity of information leakage in recursive programs. In 32nd Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS), volume 18 of Leibniz International Proceedings in Informatics, pages 534–545, 2012. Leibniz-Zentrum fuer Informatik. [pdf]

26. Rohit Chadha, P. Madhusudan and M. Viswanathan. Reachability under Contextual Locking. In 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 7214 of Lecture Notes in Computer Science, pages 437–450, 2012. Springer. [pdf]

27. Rohit Chadha, Stefan Ciobaca and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. In 22nd European Symposium on Programming (ESOP), volume 7211 of Lecture Notes in Computer Science, pages 108–127, 2012. Springer. [pdf]

28. Rohit Chadha, Vijay Korthikranthi, Mahesh Viswanathan, Gul Agha and Youngmin Kwon. Model Checking MDPs with A Unique Compact Invariant Set of Distributions. In Eighth International Conference on Quantitative Evaluation of SysTems (QEST), pages 121-130, 2011. IEEE Computer Society. [pdf]

29. Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Probablistic Buchi automata with non-extremal acceptance thresholds. In Twelfth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 103–117, 2011. [pdf]

30. Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Model checking concurrent programs with nondeterminism and randomization. In Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS), volume 8 of Leibniz International Proceedings in Informatics, pages 364–375, 2010. Leibniz-Zentrum fu ̈r Informatik. [pdf]

31. Rohit Chadha, Axel Legay, Pavithra Prabhakar, and Mahesh Viswanathan. Complexity bounds for the verification of real-time software. In Proceedings of the 11th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), volume 5944 of Lecture Notes in Computer Science, pages 95–111, 2010. Springer. [pdf]

32. Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Power of randomization in automata on infinite strings. In Proceedings of the 20th International Conference on Concurrency Theory (CONCUR), volume 5710 of Lecture Notes in Computer Science, pages 229–243, Bologna, Italy, September 2009. Springer. [pdf]

33. Rohit Chadha, Stephanie Delaune, and Steve Kremer. Epistemic logic for the applied pi calculus. In Proceedings of IFIP International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE), volume 5522 of Lecture Notes in Computer Science, pages 182–197, Lisbon, Portugal, June 2009. Springer. [pdf]

34. Rohit Chadha, Mahesh Viswanathan, and Ramesh Viswanathan. Least upper bounds for probability measures and their applications to abstractions. In 19th International Conference on Concurrency Theory (CONCUR), volume 5201 of Lecture Notes in Computer Science, pages 264–278. Springer, August 2008. [pdf]

35. 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), pages 18–29. IEEE Computer Society, June 2008. [pdf]

36. Rohit Chadha, Carl A. Gunter, Jose Meseguer, Ravinder Shankesi, and Mahesh Viswanathan. Modular preservation of safety properties by cookie-based dos-protection wrappers. In 10th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), volume 5051 of Lecture Notes in Computer Science, pages 39–58. Springer, March 2008. [pdf]

37. Rohit Chadha and Mahesh Viswanathan. Decidability results for well-structured transition systems with auxiliary storage. In 18th International Conference on Concurrency Theory (CONCUR), volume 4703 of Lecture Notes in Computer Science, pages 136–150. Springer, September 2007. [pdf]

38. Pedro Baltazar, Rohit Chadha, Paulo Mateus and Amilcar Sernadas. Towards Model-Checking Quantum Security Protocols. In First International Conference on Quantum, Nano, and Micro Technologies (ICQNM), pages 14. IEEE Computer Society, January 2007. [pdf]

39. Rohit Chadha, Paulo Mateus, and Amilcar Sernadas. Reasoning about states of probabilistic sequential programs. In Computer Science Logic, 20th International Workshop (CSL), volume 4207 of Lecture Notes in Computer Science, pages 240–255. Springer, September 2006. [pdf]

40. Rohit Chadha, Steve Kremer, and Andre Scedrov. Formal analysis of multi-party contract signing. In 17th IEEE Computer Security Foundations Workshop (CSFW), pages 266–279. IEEE Computer Society, 2004. [pdf]

41. Rohit Chadha, John Mitchell, Andre Scedrov, and Vitaly Shmatikov. Contract signing, optimism and advantage. In 14th International Conference on Concurrency Theory (CONCUR), pages 366–382. Springer-Verlag, 2003. [pdf]

42. Rohit Chadha, Max Kanovich, and Andre Scedrov. Inductive methods and contract-signing protocols. In 8th ACM Conference on Computer and Communications Security (CCS), pages 176–185. ACM Press, 2001. [pdf]

Other Publications/ Preprints

1. Bishnu Bhusal, Yuanye Ma, Rohit Chadha. Privacy Nutrition Labels: Promise, Practice, and Paradoxes in Communicating Privacy. Poster at 27th Human Computer Interaction International (HCII), 2025. Accepted.

2. Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla and Mahesh Viswanathan. Automated methods for checking differential privacy. [Arxiv preprint]

3. Gergei Bana and Rohit Chadha. Verification Methods for the Computationally Complete Symbolic Attacker Based on Indistinguishability. [IACR peprint]