Susmit Jha

 

Old Homepage

 

 

 

EDUCATION

 

• Ph.D. in Electrical Engineering and Computer Science

University of California, Berkeley  

Research Advisor: Professor Sanjit A. Seshia

Thesis Title: Towards Automated System Synthesis Using Sciduction

 

• M.S. in Electrical Engineering and Computer Science

University of California, Berkeley  

 

• B.Tech (Hons) in Computer Science and Engineering

Indian Institute of Technology, Kharagpur  

Thesis Title: Counter-example Guided System Composition From Components

 

 

EMPLOYMENT

 

 

• Research Scientist

Intel, Hillsboro (January, 2012-present)

Duties: Research on automated synthesis at Strategic CAD Lab.

Supervisor: Dr. Mike Kishinevsky

 

• Graduate Student Researcher

UC Berkeley, Berkeley (August, 2006-December 2011)

Duties: Research on mathematical logic based techniques for automated system synthesis.

Supervisor: Professor Sanjit A. Seshia

 

• Student Research Associate (Intern, on leave from UC Berkeley)

SRI International, Menlo Park (May, 2009-August,2009; May, 2010-August,2010) Duties: Research on automated program synthesis

Supervisor: Dr. Ashish Tiwari

 

• Research Intern

EPFL, Lausanne, Switzerland (May, 2005-July,2005)

Duties: Research on model identification in systems biology

Supervisor: Professor Thomas Henzinger

 

• Research Intern

Tata Institute of Fundamental Research(May, 2004-July,2004)

Duties: Research on model checking biochemical pathways

Supervisor: Professor R.K. Shyamasundar

 

PUBLICATION LIST

 

Total number of publications: 25  

Total number of citations to my publications1: 253

 

 

1 According to Google Scholar, 05/26/2013

 

 

REFEREED PROCEEDING CHAPTERS AND JOURNAL PAPERS

1.      Susmit Jha and Sanjit A. Seshia. Synthesis of Optimal Fixed-Point Implementations of Numerical Software Routines. In Proc. Sixth International Workshop on Numerical Software Verification (NSV), April 2013.

2.      Wenchao Li, Susmit Jha and Sanjit A. Seshia. Generating Control Logic for Optimized Soft Error Resilience. In Proc. 9th Workshop on Silicon Errors in Logic - System Effects (SELSE), March 2013.

3.      Sumit. K. Jha, R. G. Datta, C.J. Langmead, Susmit Jha, E. Sassano  “Synthesis of Insulin Pump Con- trollers from Safety Specifications using Bayesian Model Validation”.  International Journal of Bioin- formatics Research and Applications  (invited), previous version in 10th Annual Asia Pacific Bioinfor- matics Conference (APBC), 2012 Accepted: 42/129

Citation Count: 4

 

4.      F. Hussain, R.G. Dutta, S.K. Jha, C. J. Langmead and Susmit Jha. “Parameter Discovery for Stochastic Biological Models against Temporal Behavioral Specifications using an SPRT based Metric for Simu- lated Annealing”. 2nd IEEE International Conference on Computational Advances in Bio and Medical Sciences (ICCABS), 2012 Accepted: 25/55

 

5.      A.K. Ghosh, F. Hussain, S.K. Jha, C. J. Langmead and Susmit Jha. “Decision Procedure Based Discov- ery of Rare Behaviors in Stochastic Differential Equation Models of Biological System.  2nd IEEE International Conference on Computational Advances in Bio and Medical Sciences (ICCABS), 2012 Accepted: 25/55

 

6.      Susmit Jha, Sanjit A. Seshia, and Ashish Tiwari,   “Synthesis of optimal switching logic for hybrid systems.”.  pages 107-116, Proceedings of the 11th International Conference on Embedded Software (EMSOFT) , 2011 Accepted: 27 out of over 135 

Citation Count: 11

 

7.      Sumit Gulwani, Susmit Jha, and Ashish Tiwari, “Automated modular synthesis applied to bit-vector circuits.”. pages 62-73, Proceedings of the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), 2011 Accepted: 55 out of 236

Citation Count: 45

 

8.      Susmit Jha, Sumit Gulwani, Sanjit Seshia, and Ashish Tiwari, “Oracle-guided component-based pro- gram synthesis.”. pages 315-224, Proceedings of the 32nd International Conference on Software Engi- neering (ICSE) , 2010 Accepted: 52 out of 380 

Citation Count: 47

 

9.      Susmit Jha, Sumit Gulwani, Sanjit Seshia, and Ashish Tiwari, “Synthesizing switching logic for safety and dwell-time requirements”. pages 22-31, Proceedings of the 1st International Conference on Cyber- physical Systems (ICCPS), 2010 Acceptance rate: ~25%

Citation Count: 29

 

10.   Dave King, Susmit Jha, Divya Muthukumaran, Trent Jaeger, Somesh Jha, and Sanjit A. Seshia,  “Automating security mediation placement.”. pages 327-344, Proceedings of the 19th European Symposium on Programming (ESOP), 2010  Accepted: 30 out of  121

Citation Count: 7

 

 

 

11.   Cynthia Sturton, Susmit Jha, Sanjit A. Seshia, and David Wagner,   “On voting machine design for verification and testability.”.  pages 463-476, Proceedings of the 16th ACM Conference on Computer and Communications Security (CCS), 2009  Accepted: 58 out of 315

Citation Count: 13

 

12. Susmit Jha , Rhishikesh Limaye, and Sanjit A. Seshia, “Beaver: Engineering an efficient SMT solver for bit-vector arithmetic.”. pages 668-674, Proceedings of the 21st International Conference on Computer- Aided Verification (CAV), 2009 Accepted: <20%

Citation Count: 37

 

13. Susmit Jha, Wenchao Li, and Sanjit A. Seshia, “Localizing transient faults using dynamic Bayesian networks.”. pages 82-87, Proceedings of the 14th IEEE International High-Level Design Validation and Test (HLDVT), 2009  

Citation Count: 7

 

14. Sumit Kumar Jha and Susmit Jha, “Random relaxation abstractions for bounded reachability analysis of linear hybrid automata: Distributed randomized abstractions in model checking.”.  pages 147-153, Proceedings of the 11th IEEE High Assurance Systems Engineering Symposium, 2008 Accepted: 44 out of 196

 

15. Susmit Jha and Sumit Kumar Jha “Randomization Based Probabilistic Approach to Detect Trojan Cir- cuits”. pages 117-124, Proceedings of the 11th IEEE High Assurance Systems Engineering Symposium (HASE), 2008 Accepted:  44 out of 196

Citation Count: 26

 

16. Susmit Jha, Bryan A. Brady, and Sanjit A. Seshia, “Symbolic Reachability Analysis of Lazy Linear Hy- brid Automata.”. pages 241-256, Proceedings of the 5th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS), 2007 Accepted: 22 out of 48

      Citation Count: 20

 

17. Susmit Jha and R. K. Shyamasundar, “Adapting Biochemical Kripke Structures for Distributed Model Checking.” Pages 107-122,  Transactions on Computational Systems Biology, 2006

Citation Count: 1

 

18. Faraz Hussain, Susmit Jha, Christopher Langmead, and Sumit Kumar Jha; Parameter Discovery in Stochastic Biological Models using Simulated Annealing and Statistical Model Checking. BMC Genomics. 2013 (accepted; in press) Journal, Impact Factor: 4.07

 

19. Arup Kumar Ghosh, Susmit Jha, Christopher Langmead, and Sumit Kumar Jha; Discovering rare behaviors in stochastic differential equations using decision procedures: applications to a minimal cell cycle model. BMC Genomics. 2013 (accepted; in press) Journal, Impact Factor: 4.07

 

20. Narsingh Deo, Raj Gautam Dutta, Faraz Hussain, Susmit Jha, and Sumit Kumar Jha: Synthesizing Optimal Control Strategies for Stochastic Complex Networks. CoNeD’13 workshop affiliated with the 14th International Conference on Distributed Computing and Networking ICDCN’2013


 

 

REFEREED INTERNAL PUBLICATIONS AT Intel Corporation

 

21. Susmit Jha, Mikhail Talalay, Dan Holcomb, Umit Ogras, Michael Kishinevsky, Michael Klinglesmith, Robert De Gruijl and Seonil Choi, “Automated Design Space Exploration for SoC Interconnects” Design Technology and Tools Conference, 2013

 

22. Choi, Seonil; Davare, Abhijit; Abad, Carlos A; Toepfer, Robert J; Cai, Kui; Shen, Yingzhe; Li, Bin; Jha, Susmit; De Gruijl, Robert, “Performance Optimization Case Studies Using SystemC based Cycle Accurate PSF2.0 Model”, Design Technology and Tools Conference, 2013

 

 

TECHNICAL REPORTS AND DRAFTS UNDER SUBMISSION

 

 

23.  Susmit Jha “Statistical Analysis of Privacy and Anonymity Guarantees in Randomized Security   Protocol Implementations.”. arXiv.org, June, 2009.21.

 

24.  Susmit Jha, Sanjit A. Seshia and Rhishikesh Limaye, “On the Computational Complexity of Satisfiabil- ity Solving for String Theories.” EECS, University of California, Berkeley, March, 2009.

Citation Count: 6

 

BOOKS

25. Susmit Jha, Towards Automated System Synthesis Using SCIDUCTION Publisher: LAP Lambert Academic Publishing, 2012

ISBN 3838310683, 9783838310688

 

 

OPEN SOURCE SOFTWARE

 

26. Beaver: Bit-vector SMT Solver http://uclid.eecs.berkeley.edu/Beaver

Beaver was again ranked 3rd among all bit-vector solvers and 1st among open-source solvers in SMT- COMP09 as well as SMT-COMP08. Making it open-source facilitated other researchers in the area to experiment in bit-vector SMT solving.

Download Count:494

 

Total Citations:                                                  (253)

CITATIONS AND AWARDS

 

 

• Best Speaker Award, International Workshop on Numerical Software Verification, 2013

 

• Intel Division Recognition Award, 2012 from SoC Converged Architecture Division at Intel: “presented for developing and delivering PSF 2.0 Performance Model for lead chipset and SoC projects.”

 


 

• Leon O Chua Award, 2011 from UC Berkeley: presented annually “for outstanding achievement in an area of nonlinear science from any discipline, including biological, engineering, mathematical, physical and social sciences.”

 

• Travel Award from SIGPLAN to attend PLDI, 2011

 

• Travel Award to attend CAV, 2009

 

• Beaver SMT solver developed by me was ranked 3rd fastest bit-vector SMT solver in 2009 and 2008. It was the fastest open-source SMT solver.

 

• Berkeley Fellowship for Graduate Studies from UC Berkeley, 2006-2008

 

• TCS Gold Medal for Best Computer Science Student at IIT, Kharagpur, 2006

 

 

PRESENTATIONS AND TALKS

 

 

·        Synthesis of Device Drivers, ExSCAPE: Expeditions in Computer Augmented Program Engineering, University of California, Berkeley, US, 2013

 

·        Synthesis of Fixed Point Programs, International Workshop on Automated Program Synthesis, Philadelphia, US, 2013

 

·        Synthesis of Parameter and Policies for System-On-Chip, ExSCAPE: Expeditions in Computer Augmented Program Engineering, University of Pennsylvania, Philadelphia, US, 2012

 

·        Fixed Point Program Synthesis, IFIP meeting on Verified Software, SRI International, Menlo Park, US, 2011

 

·        Synthesis of Loop-Free Programs, International Conference on Programming Languages Design and Implementation, Federated Computing Research Conference, San Jose, US, 2011.

 

·        Switching Logic Synthesis for Cyber-Physical Systems, General Motors Research, Bangalore, India, 2010.

 

·        Program Synthesis from I/O Examples, Microsoft Research, Bangalore, India, 2010.

 

·        Synthesizing Switching Logic for Safety and Dwell-Time Requirements, International Conference on Cyber Physical Systems, Embedded Systems Week, Stockholm, Sweden, 2010.

 

·        Oracle-guided component-based program synthesis, International Conference on Software Engineering, Cape Town, South Africa, 2010.

 

·        Beaver: Engineering an efficient SMT solver for bit-vector arithmetic, International Conference on Computer-Aided Verification, Grenoble, France, 2009.

 

·        SMT solving for non-linear bit-vector arithmetic, Open Source Quality Retreat, Santa Cruz, USA, 2008.

 

 


 

EXTERNAL PROFESSIONAL ACTIVITIES

 

 

MEMBERSHIP IN PROFESSIONAL SOCIETIES

 

• IEEE Senior Member

• ACM

• Sigma Xi – Full Member

 

 

 PROGRAM COMMITTEE AND JOURNAL EDITORSHIP

 

• Executive Editor, Journal of Information Technology and Software Engineering

 

• International Conference on Formal Methods in Computer Aided Design, Portland, USA, October 20-23, 2013

 

• International Conference on Computer Aided Verification (CAV), Saint Petersburg, Russia, July 13-19, 2013

 

• CoNeD 2013: Complex Networks Dynamics: Cross-Disciplinary Tools for Modeling, Analysis, and Design, Tata Institute of Fundamental Research, Mumbai, India, 2013

 

• IEEE SoutheastCon, Jacksonville, FL, USA, April 4-7, 2013

 

• International Workshop on Model-Based Design with a Focus on Extra-Functional Properties (MB- DEFP), October 13th 2011, Taipei, Taiwan in conjunction with the Embedded Systems Week, 2011

 

 

JOURNAL REVIEWING

 

 

• Annals of Mathematics and Artificial Intelligence: Special issue on Application of Constraints to Formal

Verification and Artificial Intelligence

 

• IEEE Embedded System Letters

 

• Embedded Hardware Design (Microprocessors and Microsystems)

 

• IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

 

• International Journal on Software Tools for Technology Transfer

 

• Formal Aspects of Computing

 

• IEEE Transactions on Software Engineering

 

 

CONFERENCE REVIEWING

 

 

• International Conference on Formal Methods in Computer Aided Design, Portland, USA, 2013

 

• International Conference on Computer Aided Verification, St. Petersburg, Russia, 2013

 


 

• International Symposium on Networks on Chips, Tempe, Arizona, US, 2013

 

• Design and Automation Conference, Austin, Texas, US, 2013

 

• IEEE International Conference on Computer Design, Montreal, Canada, 2012

 

• Computer-Aided Verification, San Francisco, US, 2012

 

• International Conference on The Theory and Applications of Satisfiability Testing, Trento, Italy, 2012

 

• Design, Automation, and Test in Europe, Grenoble, France, 2011

 

• IEEE International Symposium on Circuits and Systems, Rio de Janeiro, Brazil, 2011

 

• Asia and South Pacific Design Automation Conference, Pacifico Yokohama, Yokohama, Japan, 2011

 

• Tools and Algorithms for the Construction and Analysis of Systems, Saarbrcken, Germany, 2011

 

• NASA Formal Methods Symposium, Pasadena, US, 2011

 

• Computer-Aided Verification, Snowbird, Utah, US, 2011

 

• Design, Automation, and Test in Europe, Dresden, Germany, 2010

 

• Asia and South Pacific Design Automation Conference, Taipei, Taiwan, 2010

 

• International Society for Quality Electronic Design, Santa Clara, US, 2010

 

• IEEE International Symposium on Circuits and Systems, Paris, France, 2010

 

• Tools and Algorithms for the Construction and Analysis of Systems, Paphos, Cyprus, 2010

 

• IEEE International High Level Design Validation and Test, San Francisco, US, 2009

 

• Formal Methods in Computer Aided Design, Austin, Texas, US, 2009

 

• International Conference on Computer-Aided Design, San Jose, US, 2009

 

• Constraints in Formal Verification, Grenoble, France, 2009

 

• Computer-Aided Verification, Grenoble, France, 2009

 

• Current Trends in Theory and Practice of Computer Science, pindlerv Mln, Czech Republic, 2009

 

• Formal Modelling and Analysis of Timed Systems, Budapest, Hungary, 2009

 

• International Conference on Computer-Aided Design, San Jose, US, 2008