Susmit Jha (Susmit Kumar Jha) M.S. & Ph.D., 2011 Electrical Engineering and Computer Science, University of California, Berkeley B.Tech., 2006 Computer Science, Indian Institute of Technology, Kharagpur (IIT, Kgp)

• Brief Bio
  
  • I graduated with a Ph.D. in 2011 from the Department of Electrical Engineering and Computer Science at UC, Berkeley. My graduate advisor was Professor Sanjit Seshia , and my thesis committee consisted of Professor Claire Tomlin and Professor Dorit Hochbaum . Before Berkeley, I spent four lovely years (2002-2006) at IIT Kharagpur (the oldest of all IITs) doing my undergrad in Computer Science and Engineering.


• Resume (pdf)


• News
Starting as Research Scientist in CAD Lab at Intel Portland in fall end.
Awarded Leon O. Chua Award, 2011

• Research: My graduate research focused on developing techniques for automated formal verification and synthesis of systems which can aid developers and design engineers. Our techniques are based on a combination of algorithmic learning and formal verification methods. My research areas of interest are formal methods and machine learning .

15. Susmit Jha and Sanjit A. Seshia. Automated Synthesis of Fixed-Point Numerical Code (Submitted) [Coming Soon: abstract | pdf |  bibtex ]

14. Susmit Jha , Sanjit A. Seshia and Ashish Tiwari. Synthesizing Switching Logic to Minimize Long-Run Cost. To appear in 11th International Conference on Embedded Software (EMSOFT) , 2011. [ abstract | pdf |  bibtex ]

13. Wenchao Li, Susmit Jha and Sanjit Seshia. Power-Aware Dynamic Control of Error-Resilience Mechanisms Submitted

12. Sumit Gulwani, Susmit Jha , Ashish Tiwari and Ramarathnam Venkatesan. Synthesis of Loop-Free Programs. In 32nd ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI) , pages 62-73, 2011. [ abstract | pdf |  bibtex ]

11. Susmit Jha , Sumit Gulwani, Sanjit Seshia, and Ashish Tiwari. Synthesizing Switching Logic for Safety and Dwell-Time Requirements. In International Conference on Cyber-Physical Systems (ICCPS) , pages 22-31, 2010. [ abstract | pdf |  bibtex ]

10. Susmit Jha , Sumit Gulwani, Sanjit Seshia, and Ashish Tiwari. Oracle-guided component-based program synthesis. In 32nd International Conference on Software Engineering (ICSE) , pages 315-224, 2010. [ abstract | pdf |  bibtex ]

9. David H. King, Susmit Jha , Divya Muthukumaran, Trent Jaeger, Somesh Jha, and Sanjit Seshia. Automating security mediation placement. In 19th European Symposium on Programming (ESOP) , pages 327-344, 2010. [ abstract | pdf |  bibtex ]

8. Cynthia Sturton, Susmit Jha , Sanjit A. Seshia, and David Wagner. On voting machine design for verification and testability. In 16th ACM Conference on Computer and Communications Security (ACM CCS) , pages 463-476, 2009. [ abstract | pdf | bibtex | http ]

7. Susmit Jha , Rhishikesh Limaye, and Sanjit A. Seshia. Beaver: Engineering an efficient SMT solver for bit-vector arithmetic. In 21st International Conference on Computer-Aided Verification (CAV) , pages 668-674, 2009. [ abstract | pdf | bibtex]

6. Sumit Jha and Susmit Jha Localizing Error in Traces With Interpolants. In 3rd India Software Engineering Conference (ISEC) , 2010. [ pdf | bib ]

5. Susmit Jha , Wenchao Li, and Sanjit A. Seshia. Localizing transient faults using dynamic Bayesian networks. In 14th IEEE International High-Level Design Validation and Test Workshop , 2009. [ pdf | bib ]

4. Susmit Jha and Sumit Kumar Jha. Randomization based probabilistic approach to detect Trojan circuits. In 11th IEEE High Assurance Systems Engineering Symposium , pages 117-124, 2008. [ pdf | bib ]

3. Sumit Kumar Jha and Susmit Jha . Random relaxation abstractions for bounded reachability analysis of linear hybrid automata: Distributed randomized abstractions in model checking. In 11th IEEE High Assurance Systems Engineering Symposium , pages 147-153, 2008. [ pdf | bib ]

2. Susmit Jha , Bryan A. Brady, and Sanjit ;A. Seshia. Symbolic Reachability Analysis of Lazy Linear Hybrid Automata. In 5th International Conference on Formal Modeling and Analysis of Timed Systems , pages 241-256, 2007. [ pdf | bib]

1. Susmit Jha and R. K. Shyamasundar. Adapting Biochemical Kripke Structures for Distributed Model Checking. Transactions on Computational Systems Biology , pages 107-122, 2006. [ pdf | bib]

Technical Reports

1.Susmit Jha, Sanjit A. Seshia, Rhishikesh Limaye: On the Computational Complexity of Satisfiability Solving for String Theories CoRR abs/0903.2825: (2009) Weblink

2.Susmit Jha: Statistical Analysis of Privacy and Anonymity Guarantees in Randomized Security Protocol Implementations CoRR abs/0906.5110: (2009) Weblink

3.Stochastic modeling and analysis of Circadian Clock Pathway. (2006) Weblink

Tool Releases

1. Bitvector Decision Procedure Beaver-1.0 is available for download here. It is a theorem prover for bit-vector logic. CAV 2009 paper on Beaver is available here. (Work with Rhishi and Sanjit)

News: Beaver was again ranked 3 among all bit-vector solvers and 1 among open-source solvers in SMT-COMP09 - the same ranks as in SMT-COMP08.

2. IFC Solver for solving information flow constraints from Java Information Flow language.

Please send me a mail if you are interested in obtaining the implementation of any of my papers.

Sumit Gulwani, Susmit Jha , Ashish Tiwari and Ramarathnam Venkatesan. Synthesis of Loop-Free Programs. In 32nd ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI) , 2011. [Slides(pdf)]

Susmit Jha , Sumit Gulwani, Sanjit Seshia, and Ashish Tiwari. Synthesizing Switching Logic for Safety and Dwell-Time Requirements. In International Conference on Cyber-Physical Systems (ICCPS) , 2010. [Slides(pdf)]

Susmit Jha , Sumit Gulwani, Sanjit Seshia, and Ashish Tiwari. Oracle-guided component-based program synthesis. In 32nd International Conference on Software Engineering (ICSE) , 2010. [Slides(pdf)]

Susmit Jha , Rhishikesh Limaye, and Sanjit A. Seshia. Beaver: Engineering an efficient SMT solver for bit-vector arithmetic. In 21st International Conference on Computer-Aided Verification (CAV) , 2009. [Slides(pdf)]

Work Experience

Summer, 2010: Student Associate (Cyberphysical System Controller Synthesis), SRI International, Menlo Park, CA. Mentor: Dr. Ashish Tiwari

Summer, 2009: Student Associate (Program Synthesis), SRI International, Menlo Park, CA. Mentor: Dr. Ashish Tiwari

Summer, 2005: Research Intern (Computational Systems Biology), EPFL, Lausanne, Switzerland. Mentor: Professor Thomas Henzinger, Dr. Jasmin Fischer, Dr. Nir Piterman

Summer, 2004: Indian Academy of Sciences Research Fellow (Program Verification), Tata Institute of Fundamental Research, Bombay, India. Mentor: Professor R. K. Shyamasundar

Misc

Other Research Activities:

Reviewed papers for

Journals:
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

Conferences:
2011: DATE, ISCAS, ASP-DAC, TACAS, NASA FM, CAV
2010: DATE, ASP-DAC, ISQED, ISCAS, TACAS
2009: HLDVT, FMCAD, ICCAD, CFV, FORMATS, CAV, SOFSEM
2008: ICCAD


When not at work:
Well, have been planning for long to blog and EF(blog)
Reading - mainly non-fiction but Asimov remains my ever-favorite
Coding for fun: Am an Emacs/bash guy with new found love for scripting languages.


Links:
Graam by Saryu Prasad Mishra Aanand
Haar by Saryu Prasad Mishra Aanand
My brother Sumit Jha's Home Page
Tennyson's Ulysses
'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; ....

Contact Info