Skip to main content


Office Location

440 Huntington Avenue
330 West Village H
Boston, MA 02115


Harsh Raju Chamarthi is a PhD student in the Computer Science program at Northeastern University’s College of Computer and Information Science, advised by Professor Pete Manolios. Harsh graduated from the Indian Institute of Technology, Kanpur in 2002, where he earned a bachelor’s degree in electrical engineering. After graduating from IIT, Harsh Raju worked as a Software Engineer for many years in Bangalore. His field of study is formal methods.


  • BTech, Indian Institute of Technology – India

About Me

What are the specifics of your graduate education (thus far)?

I took courses in Logic, Programming Languages, Theory of Computation, Compilers, etc. I also taught Logic and Computation for one semester.

What are your research interests?

My research (and implementation) effort is aimed at Counterexample Generation for ACL2, an interactive theorem prover.

What’s one problem you’d like to solve with your research/work?

Better support for interactive non-theorem disproving.

What aspect of what you do is most interesting?

The “interactive” aspect; most current theorem-proving research is aimed at automation.

What are your research or career goals, going forward?

Study all aspects of theorem proving more deeply.