Susmit Jha

Principal Computer Scientist,
Computer Science Laboratory, SRI International
Email: susmit.jha at sri.com, 51 0- 3 25- 70 12

Past:
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)

Susmit Jha is a Principal Scientist at SRI International, leading the research thrust on trust, resilience, and interpretability of AI. His research focuses on combining formal methods and machine learning to build trusted artificial intelligence and correct-by-construction autonomous systems. His research background is in Formal Methods, Artificial Intelligence and Control Theory. His current projects are:

News : We have been selected to perform on:

Previous Projects: DARPA SW Symmetry, 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. 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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  27. A Theory of Formal Synthesis via Inductive Learning.
    Susmit Jha and Sanjit Seshia.

    Acta Informatica, 2017
    Paper (PDF)

  28. 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)
  29. 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)
  30. 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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Selected Awards and Honors

2020 Most Influencial Paper Award at 42nd International Conference on Software Engineering, 2020 (10 year influence award for our paper on Oracle-guided Program Synthesis at ICSE 2010) ICSE 2020  
2019 Best Demo Award at HSCC 2019 for Neural Network Verification Tool Sherlock  
2018 SRI CSL Spot Award for Research Leadership on DARPA SW Symmetry Project  
2016 UTRC Great Job Award for DARPA Project on Communication Under Contested Environment  
2014 Research Scoping Award for Low Energy Platforms, Intel  
2012 SoC Converged Architecture Recognition Award for Automated NoC Synthesis for 14nm SoCs, Intel  
2011 Leon Chua Award, UC Berkeley  
2006-2008 Berkeley Fellowship for Graduate Studies  
2006 TCS Gold Medal, IIT Kharagpur  
2000-2006 NTSE Scholar (India)  

- ---- -----


'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; ....