Susmit Jha

Technical Director, NuSCI Research Group,
Computer Science Laboratory, SRI International
Email: firstname.lastname at sri.com

Past:
Principal Computer Scientist, SRI (Dec, 2019 - Sept, 2022)
Senior Staff Scientist, SRI (Oct, 2016 - Dec, 2019)
Staff Research Scientist, UTRC (Raytheon Technologies) , Berkeley (Dec, 2014 - Oct, 2016)
Research Scientist, Intel, Hillsboro (Jan, 2012 - Dec, 2014)
M.S. and Ph.D., EECS, UC Berkeley (Aug, 2006 - Dec, 2011)
B.Tech., Dept. of Computer Science, IIT Kharagpur (2002-2006)

Bio: Dr. Susmit Jha is a Technical Director in the Computer Science Laboratory at SRI International , where he leads the research group on Neuro-symbolic Computing and Intelligence. His research focuses on combining formal methods, machine learning, and control theory to build trusted artificial intelligence and correct-by-construction autonomous systems. Dr. Jha completed his Ph.D. in Computer Science from UC Berkeley in 2011, where his thesis work on “Automated Synthesis Using Structurally Constrained Induction and Deduction” was supported by the Berkeley Fellowship and was awarded the Leon O Chua Award. Before joining SRI, Dr. Jha was at Intel Strategic CAD Labs and Raytheon Technologies Research Center at Berkeley. At Intel, Dr. Jha’s research received a Division Recognition Award in 2012 and a Research Technology Scoping Award in 2014. He is the recipient of the 10-year Most Influential Paper award at IEEE/ACM ICSE 2020 . He has published over 80 peer-reviewed publications with over 3400 citations in AI, ML, and automated reasoning venues such as NeurIPS, ICLR, ICML, CVPR, ICCV, AAAI, IJCAI, JAR, PLDI, and CAV. Dr. Jha has been a Principal Investigator on DoD and other US Govt. programs on trustworthy, resilient, and neuro-symbolic AI, including:

The Defense Advanced Research Projects Agency (DARPA) has named Dr. Susmit Jha to the Information Science & Technology (ISAT) Study Group beginning in July 2023. The group identifies new areas of development in computer science and information technology and to recommend future possible research directions. The ISAT Study Group was established by DARPA in 1987 to support its technology offices and provide continuing and independent assessment of the state of advanced Information Science technology as it relates to the U.S. Department of Defense.

Previous DoD Projects: DARPA IDAS , DARPA RFMLS , DARPA BRASS , DARPA MUSE , DARPA SoSITE , DARPA C2E , and DARPA ALIAS .

PhD Thesis

Publications

Preprints

Misc.

Dagstuhl Seminar 17351

Peer-Reviewed Publications ( in Reverse Chronological Order )

  1. Direct Amortized Likelihood Ratio Estimation
    Adam Cobb, Brian Matejek, Daniel Elenius, Anirban Roy, Susmit Jha:
    38th Annual AAAI Conference on Artificial Intelligence (AAAI), 2024
    Paper (PDF)

  2. Principled Out-of-Distribution Detection via Multiple Testing
    Akshayaa Magesh, Venugopal V. Veeravalli, Anirban Roy, Susmit Jha
    Journal of Machine Learning Research, 2023
    Paper (PDF)

  3. AircraftVerse: A Large-Scale Multimodal Dataset of Aerial Vehicle Designs
    Adam D. Cobb, Anirban Roy, Daniel Elenius, Frederick Michael Heim, Brian Swenson, Sydney Whittington, James D Walker, Theodore Bapty, Joseph Hite, Karthik Ramani, Christopher McComb, Susmit Jha
    Thirty-seventh Conference on Neural Information Processing Systems (NeurIPS), 2023 (Benchmarks and Datasets)
    Paper (PDF)

  4. Direct Amortized Likelihood Ratio Estimation
    Adam D. Cobb, Brian Matejek, Daniel Elenius, Anirban Roy, Susmit Jha
    NeurIPS workshop on Machine Learning and the Physical Sciences, 2023
    Paper (PDF)

  5. Universal Trojan Signatures in Reinforcement Learning
    Manoj Acharya, Weichao Zhou, Anirban Roy, Xiao Lin, Wenchao Li, Susmit Jha
    NeurIPS Workshop on Backdoors in Deep Learning, 2023
    Paper (PDF)

  6. TIJO: Trigger Inversion with Joint Optimization for Defending Multimodal Backdoored Models
    Indranil Sur, Karan Sikka, Matt Walmer, Kaushik Koneripalli, Anirban Roy, Xiao Lin, Ajay Divakaran, Susmit Jha
    International Conference on Computer Vision (ICCV) 2023
    Paper (PDF)

  7. Counterexample Guided Inductive Synthesis Using Large Language Models and Satisfiability Solving
    Sumit Jha, Susmit Jha, Pat Lincoln, Nate D. Bastian, Alvaro Velasquez, Rickard Ewetz, Sandeep Neema
    IEEE Military Communications Conference (MILCOM) 2023
    Paper (PDF)

  8. Neural SDEs for Robust and Explainable Analysis of Electromagnetic Unintended Radiated Emissions
    Sumit Jha, Susmit Jha, Rickard Ewetz, Alvaro Velasquez
    IEEE Military Communications Conference (MILCOM) 2023
    Paper (PDF)

  9. Dehallucinating Large Language Models Using Formal Methods Guided Iterative Prompting
    Susmit Jha, Sumit Jha, Pat Lincoln, Nate D. Bastian, Alvaro Velasquez, Sandeep Neema
    IEEE International Conference on Assured Autonomy (ICAA) 2023
    Paper (PDF)

  10. Predicting Out-of-Distribution Performance of Deep Neural Networks Using Model Conformance
    Ramneet Kaur, Susmit Jha, Anirban Roy, Oleg Sokolsky, Insup Lee
    IEEE International Conference on Assured Autonomy (ICAA) 2023
    Paper (PDF)

  11. Detecting Trojaned DNNs using counterfactual attributions
    Karan Sikka, Indranil Sur, Anirban Roy, Ajay Divakaran, Susmit Jha
    IEEE International Conference on Assured Autonomy (ICAA) 2023
    Paper (PDF)

  12. Principled OOD Detection via Multiple Testing
    Askhayaa Magesh, Venu V Veeravalli, Susmit Jha, Anirban Roy
    IEEE International Symposium on Information Theory 2023
    Paper (PDF)

  13. CODiT: Conformal Out-of-Distribution Detection in Time-Series Data for Cyber-Physical Systems.
    Ramneet Kaur, Kaustubh Sridhar, Sangdon Park, Yahan Yang, Susmit Jha, Anirban Roy, Oleg Sokolsky, and Insup Lee.
    ACM/IEEE 14th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2023)
    Paper (PDF) Code

  14. Characterizing the 1s:E state in the 28-Si:77-Se+ spin-photon system by the equation-of-motion variational quantum eigensolver method
    Cody Fan, Adam Cobb, Murat Sarihan, Jiahui Huang, Jin Ho Kang, Khalifa Azizur-Rahman, Susmit Jha, Chee Wei Wong
    Bulletin of the American Physical Society
    Paper (PDF)

  15. Responsible Reasoning with Large Language Models and the Impact of Proper Nouns.
    Sumit Jha, Rickard Ewetz, Alvaro Velasquez, and Susmit Jha.
    Workshop on Trustworthy and Socially Responsible Machine Learning, NeurIPS 2022
    Paper (PDF)

  16. Principal Manifold Flows.
    Edmond Cunningham, Adam Cobb, Susmit Jha
    39th International Conference on Machine Learning (ICML), 2022.
    Paper (PDF)

  17. Dual-Key Multimodal Backdoors for Visual Question Answering.
    Walmer, Matthew, Karan Sikka, Indranil Sur, Abhinav Shrivastava, and Susmit Jha
    IEEE / CVF Computer Vision and Pattern Recognition Conference (CVPR), 2022.
    Paper (PDF)

  18. Detecting out-of-context objects using graph contextual reasoning network.
    Manoj Acharya, Anirban Roy, Kaushik Koneripalli, Susmit Jha, Christopher Kanan, Ajay Divakaran
    31st International Joint Conference on Artificial Intelligence (IJCAI), 2022.
    Paper (PDF)

  19. Trigger Hunting with a Topological Prior for Trojan Detection.
    Xiaoling Hu, Xiao Lin, Michael Cogswell, Yi Yao, Susmit Jha, Chao Chen
    10th International Conference on Learning Representations (ICLR), 2022.
    Paper (PDF)

  20. Runtime monitoring of deep neural networks using top-down context models inspired by predictive processing and dual process theory.
    Anirban Roy, Adam Cobb, Nathaniel Bastian, Brian Jalaian, and Susmit Jha
    AAAI Spring Symposium 2022.
    Paper (PDF)

  21. Context-aware Collaborative Neuro-Symbolic Inference in IoBTs.
    Tarek Abdelzaher, Nathaniel D. Bastian, Susmit Jha, Lance Kaplan, Mani Srivastava, and Venugopal V. Veeravalli.
    IEEE Military Communications Conference (MILCOM), IEEE, 2022.
    Paper (PDF)

  22. iDECODe: In-distribution Equivariance for Conformal Out-of-distribution Detection
    Ramneet Kaur, Susmit Jha, Anirban Roy, Sangdon Park, Edgar Dobriban, Oleg Sokolsky, Insup Lee
    36th AAAI Conference on Artificial Intelligence (AAAI), 2022
    Paper (PDF)

  23. Shaping Noise for Robust Attributions in Neural Stochastic Differential Equations
    Sumit Jha, Rickard Ewetz, Alvaro Velasquez, Arvind Ramanathan, Susmit Jha
    36th AAAI Conference on Artificial Intelligence (AAAI), 2022
    Paper (PDF)

  24. On Diverse System-Level Design Using Manifold Learning and Partial Simulated Annealing.
    Cobb, Adam, Anirban Roy, Daniel Elenius, Kaushik Koneripalli, and Susmit Jha.
    Proceedings of the Design Society 2: 1541-1548, 2022 Top 10% Paper Award
    Paper (PDF)

  25. Trinity AI Co-Designer for Hierarchical Oracle-guided Design of Cyber-Physical Systems
    Adam Cobb, Anirban Roy, Daniel Elenius, and Susmit Jha.
    IEEE Workshop on Design Automation for CPS and IoT (DESTION), 2022
    Paper (PDF)

  26. Principles of Robust Learning and Inference for IoBTs
    Nathaniel D Bastian, Susmit Jha, Paulo Tabuada, Venugopal Veeravalli, Gunjan Verma
    Book: IoT for Defense and National Security
    Paper (PDF)

  27. On Detection of Out of Distribution Inputs in Deep Neural Networks
    Susmit Jha, Anirban Roy
    IEEE 3rd International Conference on Cognitive Machine Intelligence (CogMI), 2021
    Paper (PDF)

  28. On Smoother Attributions using Neural Stochastic Differential Equations
    Sumit Jha, Rickard Ewetz, Alvaro Velasquez, Susmit Jha
    30th International Joint Conference on Artificial Intelligence (IJCAI), 2021
    Paper (PDF)

  29. Trinity: Trust, Resilience and Interpretability of Machine Learning Models
    Susmit Jha, Brian Jalaian, Anirban Roy, Gunjan Verma
    Game Theory and Machine Learning for Cyber Security (Book, 2021)
    Paper (PDF)

  30. Detecting OODs as datapoints with High Uncertainty
    Ramneet Kaur, Susmit Jha, Anirban Roy, Sangdon Park, Oleg Sokolsky, Insup Lee
    Uncertainty & Robustness in Deep Learning Workshop @ ICML 2021
    Paper (PDF)

  31. MISA: Online Defense of Trojaned Models using Misattributions
    Panagiota Kiourti, Wenchao Li, Anirban Roy, Karan Sikka, Susmit Jha
    ACSAC 2021
    Paper (PDF)

  32. Automated Synthesis of Quantum Circuits using Symbolic Abstractions and Decision Procedures
    Alvaro Velasquez, Sumit Kumar Jha, Rickard Ewetz, Susmit Jha
    54th IEEE International Symposium on Circuits and Systems (ISCAS) 2021
    Paper (PDF)

  33. Learning Certified Control Using Contraction Metric
    Dawei Sun, Susmit Jha, Chuchu Fan.
    Conference on Robot Learning (CoRL) 2020
    Paper (PDF)

  34. On the Need for Topology-Aware Generative Models for Manifold-Based Defenses
    Uyeong Jang, Susmit Jha, Somesh Jha
    8th International Conference on Learning Representations (ICLR) 2020
    Paper (PDF)

  35. Estimating the Density of States of Boolean Satisfiability Problems on Classical and Quantum Computing Platforms
    Tuhin Sahai, Anurag Mishra, Jose Miguel Pasini, Susmit Jha.
    34th AAAI Conference on Artificial Intelligence (AAAI) 2020 (Oral)
    Paper (PDF)

  36. Model-Centered Assurance for Autonomous Systems
    Susmit Jha, John Rushby and Natarajan Shankar
    39th International Conference on Computer Safety, Reliability and Security (SafeComp), 2020
    Paper (PDF)

  37. TrojDRL: Trojan Attacks on Deep Reinforcement Learning Agents
    Panagiota Kiourti, Kacper Wardega, Susmit Jha and Wenchao Li.
    57th ACM/IEEE Design Automation Conference (DAC), July 2020
    Paper (PDF)

  38. Attribution-Based Confidence (ABC) Metric For Deep Neural Networks
    Susmit Jha, Sunny Raj, Steven Fernandes, Sumit Kumar Jha, Somesh Jha, Jalaian Brian, Gunjan Verma and Ananthram Swami.
    Thirty-third Conference on Neural Information Processing Systems (NeurIPS) 2019
    Paper (PDF)

  39. TRINITY: Trust, Resilience and Interpretability of AI (Tutorial)
    Susmit Jha
    12th Workshop on Numerical Software Verification 2019
    Paper | Slides (PDF)

  40. Logic Extraction for Explainable AI
    Susmit Jha
    Workshop on Formal Methods for ML-Enabled Autonomous Systems Affiliated with CAV 2019
    Paper (PDF) | Slides (PDF)

  41. Attribution-driven Causal Analysis for Detection of Adversarial Examples.
    Susmit Jha, Sunny Raj, Steven Fernandes, Sumit Kumar Jha, Somesh Jha, Jalaian Brian, Gunjan Verma and Ananthram Swami.
    Workshop on Safe Machine Learning: Specification, Robustness and Assurance at International Conference on Learning Representations (SafeML/ICLR), 2019
    Paper (PDF)

  42. Sherlock - A Tool for Verification of Neural Network Feedback Systems: Demo Abstract. (Best Demo Award)
    Souradeep Dutta, Xin Chen, Susmit Jha, Sriram Sankaranarayanan and Ashish Tiwari.
    22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC), 2019
    Paper (PDF)

  43. TeLEx: Learning signal temporal logic from positive examples using tightness metric.
    Susmit Jha, Ashish Tiwari, Sanjit A. Seshia, Tuhin Sahai and Natarajan Shankar.
    Formal Methods in System Design (FMSD), 2019
    Paper (PDF)

  44. A Risk-Sensitive Finite-Time Reachability Approach for Safety of Stochastic Dynamic Systems.
    Margaret P. Chapman, Jonathan Lacotte, Aviv Tamar, Donggun Lee, Kevin M. Smith, Victoria Cheng, Jaime F. Fisac, Susmit Jha, Marco Pavone, Claire J. Tomlin
    IEEE American Control Conference (ACC), 2019
    Paper (PDF)

  45. Inferring and Conveying Intentionality: Beyond Numerical Rewards to Logical Intentions.
    Susmit Jha and John Rushby.
    AAAI Spring Symposium, Towards Conscious AI Systems, 2019
    Paper (PDF)

  46. Sherlock: A Tool for Verification of Deep Neural Networks.
    Souradeep Dutta, Taisa Kushner, Susmit Jha, Sriram Sankaranarayanan,Natarajan Shankar, Ashish Tiwari.
    AAAI Spring Symposium on Verification of Neural Networks (VNN), 2019.
    Paper (PDF)

  47. Learning Task Specifications from Demonstrations.
    Marcell Vazquez-Chanlatte, Susmit Jha, Ashish Tiwari, Mark K. Ho and Sanjit A. Seshia.
    32nd International Conference on Neural Information Processing Systems (NeurIPS), 2018
    Paper (PDF)

  48. Safe Autonomy Under Perception Uncertainty Using Chance-Constrained Temporal Logic.
    Susmit Jha, Vasumathi Raman, Dorsa Sadigh, and Sanjit A. Seshia.
    Journal of Automated Reasoning, 60(1):43–62, 2018.
    Paper (PDF)

  49. Data-efficient Learning of Robust Control Policies.
    Susmit Jha and Patrick Lincoln.
    56th IEEE Allerton Control Conference, 2018
    Paper (PDF)

  50. Explaining AI Decisions Using Efficient Methods for Learning Sparse Boolean Formulae.
    Susmit Jha, Tuhin Sahai, Vasumathi Raman, Alessandro Pinto and Michael Francis.
    Journal of Automated Reasoning, 2018
    Paper (PDF)

  51. Detecting Adversarial Examples Using Data Manifolds.
    Susmit Jha, Uyeong Jang, Somesh Jha and Brian Jalaian.
    IEEE Military Communications Conference (MILCOM), 2018 (Also accepted at NATO SET 262 Meeting)
    Paper (PDF)

  52. Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems.
    Susmit Jha, Sunny Raj, Sumit Kumar Jha and Natarajan Shankar.
    16th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2018.
    Paper (PDF)

  53. Learning and Verification of Feedback Control Systems using Feedforward Neural Networks.
    Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, Ashish Tiwari.
    IFAC Conference on Analysis and Design of Hybrid Systems, 2018
    Paper (PDF)

  54. Model, Data and Reward Repair: Trusted Machine Learning for Markov Decision Processes.
    Shalini Ghosh, Susmit Jha, Ashish Tiwari, Patrick Lincoln, Xiaojin Zhu.
    Workshop on Dependable and Secure Machine Learning at IEEE/IFIP International Conference on Dependable Systems and Networks (DSML/DSN), 2018.
    Paper (PDF)

  55. Output Range Analysis for Deep Feedforward Neural Networks.
    Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, Ashish Tiwari.
    NASA Formal Methods (NFM), 2018
    Paper (PDF)

  56. Trusted Neural Networks for Safety-Constrained Autonomous Control.
    Shalini Ghosh, Amaury Mercier, Dheeraj Pichapati, Susmit Jha, Vinod Yegneswaran, Patrick Lincoln.
    DISE1: Joint Workshop on Machine Learning for Safety-Critical Applications in Engineering at DISE/ICML, 2018
    Paper (PDF)

  57. Will distributed computing revolutionize peace? The emergence of battlefield IoT.
    T. Abdelzaher, N. Ayanian, T. Basar, S. Diggavi, J. Diesner, D. Ganesan, R. Govindan, S. Jha, T. Lepoint, B. Marlin, K. Nahrstedt, D. Nicol, R. Rajkumar, S. Russell, S. Seshia, F. Sha, P. Shenoy, M. Srivastava, G. Sukhatme, A. Swami, P. Tabuada, D. Towsley, N. Vaidya, and V. Veeravalli
    IEEE Int’l Conference on Distributed Computing Systems, 2018.
    Paper (URL)

  58. TeLEx: Passive STL Learning Using Only Positive Examples.
    Susmit Jha, Ashish Tiwari, Sanjit A. Seshia, Natarajan Shankar, and Tuhin Sahai.
    17th International Conference on Runtime Verification (RV), 2017
    Paper (PDF)

  59. On Learning Sparse Boolean Formulae For Explaining AI Decisions.
    Susmit Jha, Vasumathi Raman, Alessandro Pinto, Tuhin Sahai, and Michael Francis.
    NASA Formal Methods (NFM), 2017
    Paper (PDF)

  60. A Theory of Formal Synthesis via Inductive Learning.
    Susmit Jha and Sanjit Seshia.
    Acta Informatica, 2017
    Paper (PDF)

  61. On exists-forall-exists Solving: A Case Study on Automated Synthesis of Magic Card Tricks
    Susmit Jha, Vasu Raman, Sanjit Seshia.
    IEEE Formal Methods in Computer-Aided Design (FMCAD), 2016
    Paper (PDF)

  62. On Optimal Control of Stochastic Linear Hybrid Systems Controllers.
    Susmit Jha and Vasumathi Raman.
    14th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS), 2016
    Paper (PDF)

  63. Automated Synthesis of Safe Autonomous Vehicle Control Under Perception Uncertainty. (On Chance Constrained Signal Temporal Logic)
    Susmit Jha and Vasumathi Raman.
    NASA Formal Methods (NFM), 2016
    Paper (PDF)

  64. On the Teaching Dimension of Octagons for Formal Synthesis.
    Susmit Jha, Sanjit A. Seshia and Xiaojin Jerry Zhu.
    5th Workshop on Synthesis at Computer Aided Verification (SYNT/CAV), 2016
    Paper (PDF)

  65. Optimizing mobile display brightness by leveraging human visual perception.
    Matthew Schuchhardt, Susmit Jha, Raid Ayoub, Michael Kishinevsky, Gokhan Memik.
    International Conference on Compilers, Architecture and Synthesis for Embedded Systems (CASES) at ESWEEK, 2015
    Paper (PDF)

  66. Parameter discovery in stochastic biological models using simulated annealing and statistical model checking.
    Faraz Hussain, Sumit Kumar Jha, Susmit Jha, Christopher James Langmead.
    International Journal of Bioinformatics Research and Applications (IJBRA), 2014
    Paper (URL)

  67. Discovering rare behaviours in stochastic differential equations using decision procedures: applications to a minimal cell cycle model.
    Arup Kumar Ghosh, Faraz Hussain, Susmit Jha, Christopher James Langmead, Sumit Kumar Jha.
    International Journal of Bioinformatics Research and Applications (IJBRA), 2014
    Paper (URL)

  68. CAPED: Context-aware personalized display brightness for mobile devices.
    Matthew Schuchhardt, Susmit Jha, Raid Ayoub, Michael Kishinevsky, Gokhan Memik.
    International Conference on Compilers, Architecture and Synthesis for Embedded Systems (CASES) at ESWEEK, 2014
    Paper (PDF)

  69. Game theoretic secure localization in wireless sensor networks.
    Susmit Jha, Stavros Tripakis, Sanjit A. Seshia, Krishnendu Chatterjee.
    IEEE International Conference on the Internet of Things (IOT), Cambridge, MA, 2014
    Paper (PDF)

  70. Are There Good Mistakes? A Theoretical Analysis of CEGIS.
    Susmit Jha, Sanjit A. Seshia.
    Workshop on Synthesis at Federated Logic Conference/Vienna Summer of Logic (SYNT/FLoC), 2014
    Paper (PDF)

  71. Synthesis of Optimal Fixed-Point Implementation of Numerical Software Routines
    Susmit Jha, Sanjit A. Seshia
    Numerical Software Verification (NSV) collocated with CPSWeek, Philadelphia, 2013
    Paper (PDF)

  72. Automatic microarchitecture synthesis for SoCs.
    Susmit Jha, Umit Ogras, Michael Kishinevsky.
    Intel Design Tools and Technology Conference (DTTC), 2013
    Intel's annual corporate-wide, internal technical conference.

  73. Synthesis of insulin pump controllers from safety specifications using Bayesian model validation.
    Sumit Kumar Jha, Raj Gautam Dutta, Christopher James Langmead, Susmit Jha, Emily Sassano.
    International Journal of Bioinformatics Research and Applications (IJBRA), 2012
    Paper (URL)

  74. Decision procedure based discovery of rare behaviors in Stochastic Differential Equation models of biological systems.
    Arup K. Ghosh, Faraz Hussain, Sumit Kumar Jha, Christopher James Langmead, Susmit Jha.
    International Conference on Computational Advances in Bio and Medical Sciences (ICCABS), 2012
    Paper (URL)

  75. Parameter discovery for stochastic biological models against temporal behavioral specifications using an SPRT based Metric for simulated annealing.
    Faraz Hussain, Raj Gautam Dutta, Sumit Kumar Jha, Christopher James Langmead, Susmit Jha.
    International Conference on Computational Advances in Bio and Medical Sciences (ICCABS), 2012
    Paper (URL)

  76. Synthesis of loop-free programs.
    Sumit Gulwani, Susmit Jha, Ashish Tiwari, Ramarathnam Venkatesan.
    ACM SIGPLAN Programming Language Design and Implementation (PLDI), 2011
    Paper (PDF)

  77. Synthesis of optimal switching logic for hybrid systems.
    Susmit Jha, Sanjit A. Seshia, Ashish Tiwari.
    ACM SIGBED International Conference on Embedded Software (EMSOFT), 2011
    Paper (PDF)

  78. Oracle-guided component-based program synthesis.
    Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari.
    ACM/IEEE International Conference on Software Engineering (ICSE), 2010
    Paper (PDF)

  79. Automating Security Mediation Placement.
    Dave King, Susmit Jha, Divya Muthukumaran, Trent Jaeger, Somesh Jha, Sanjit A. Seshia.
    ETAPS European Symposium on Programming Languages (ESOP), 2010
    Paper (PDF)

  80. Synthesizing switching logic for safety and dwell-time requirements.
    Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, Ashish Tiwari.
    ACM/IEEE International Conference on Cyber-physical Systems (ICCPS), 2010
    Paper (PDF)

  81. Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic.
    Susmit Jha, Rhishikesh Limaye, Sanjit A. Seshia.
    International Conference on Computer-Aided Verification (CAV), 2009
    Paper (PDF)

  82. On voting machine design for verification and testability.
    Cynthia Sturton, Susmit Jha, Sanjit A. Seshia, David Wagner.
    ACM Conference on Computer and Communications Security (CCS), 2009
    Paper (PDF)

  83. Localizing transient faults using dynamic bayesian networks.
    Susmit Jha, Wenchao Li, Sanjit A. Seshia.
    IEEE High-level Design and Verification Technology (HLDVT), 2009
    Paper (PDF)

  84. Randomization Based Probabilistic Approach to Detect Trojan Circuits.
    Susmit Jha, Sumit Kumar Jha.
    IEEE High Assurance System Engineering (HASE), 2008
    Paper (URL)

  85. Random Relaxation Abstractions for Bounded Reachability Analysis of Linear Hybrid Automata.
    Sumit Kumar Jha, Susmit Jha.
    IEEE High Assurance System Engineering (HASE), 2008
    Paper (URL)

  86. Symbolic Reachability Analysis of Lazy Linear Hybrid Automata.
    Susmit Jha, Bryan A. Brady, Sanjit A. Seshia.
    International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), 2007
    Paper (PDF), Slides

  87. Adapting Biochemical Kripke Structures for Distributed Model Checking.
    Susmit Jha, R. K. Shyamasundar.
    Transactions on Computational Systems Biology, 2006
    Paper (PDF), Slides

Ph.D. Thesis

Towards Automated System Synthesis Using Sciduction, UC Berkeley, November 2011

Advisor: Sanjit A. Seshia, Rest of Thesis Committee : Claire Tomlin, Dorit Hochbaum

Executive Summary: This thesis combined learning-based induction and logical deduction to automate synthesis of programs and controllers from examples and demonstrations.

Abstract: Automated synthesis of systems that are correct by construction has been a long-standing goal of computer science. Synthesis is a creative task and requires human intuition and skill. Its complete automation is currently beyond the capacity of programs that do automated reasoning. However, there is a pressing need for tools and techniques that can automate non-intuitive and error-prone synthesis tasks. This thesis proposes a novel synthesis approach to solve such tasks in the synthesis of programs as well as the synthesis of switching logic for cyberphysical systems. The common underlying theme of the proposed synthesis techniques is a novel combination of deductive reasoning, inductive reasoning and structure hypotheses on the system under synthesis. We call this combined reasoning technique SCIDUCTION that stands for ‘Structurally Constrained Induction and Deduction’. SCIDUCTION constrains inductive and deductive reasoning using structure hypotheses, and actively combines inductive and deductive reasoning: for instance, deductive techniques generate examples for learning, and inductive techniques generate generalizations as candidate designs to be proved or disproved by deduction. We use the proposed synthesis approach for automated synthesis of loop-free programs from black-box oracle specifications using functions from a library of component functions, synthesizing optimal cost fixed-point code with specified accuracy from floating-point code, and synthesizing switching logic of hybrid systems for safety and performance properties. We illustrate that our approach can be used to automate system synthesis, and thus, can prove to be an effective aid to designers and developers.

Primary thesis papers: FORMATS'07 , CAV'09 , ICSE'10 , ICCPS'10 , PLDI'11 , EMSOFT'11

Award: Leon Chua Award, UC Berkeley, 2011 for contributions to nonlinear sciences.

Community Service

Service on U.S. Govt. agency research panels available on request.  
2020 12th NASA Formal Methods Symposium (PC Chair)  
2020 23rd ACM International Conference on Hybrid Systems: Computation and Control (PC Member)  
2019 Served as a Shark on SRI Shark Tank  
2019 NeurIPS (PC Member)
2019 AAAI Symposium on Verified Neural Networks (PC Member)
2019 Formal Methods and Machine Learning for Autonomous Systems (PC Member)
2019-2018 International Conference on Embedded Software (PC Member)
2019-2016 Numerical Software Verification (PC Member)
2018, 2014-2013 International Conference on Computer Aided Verification (PC Member)
2018-2017 NASA Formal Methods (PC Member)
2018-2015 Design Automation Conference IP Track (PC Member)
2015 Verified Software: Theories, Tools, and Experiments (PC Member)
2014 Workshop on Formal Synthesis (PC Co-Chair)
2013- Journal of Information Technology and Software Engineering (Executive Editor)
2014-2013 International Conference on Formal Methods in Computer-Aided Design (PC Member)
2013 Complex Networks Dynamics: Cross-Disciplinary Tools for Modeling, Analysis (PC Member)
2011 International Workshop on Model-Based Design (PC Member)

- ---- -----


'Tis not too late to seek a newer world.
Push off, and sitting well in order smite
the sounding furrows; for my purpose holds
To sail beyond the sunset, and the baths
Of all the western stars, until I die.
It may be that the gulfs will wash us down;
It may be that we shall touch the Happy Isles,
And see the great Achilles, whom we knew.
Though much is taken, much abides; ....