Harsh Raju Chamarthi
PhD student (since Fall 2009)
College of Computer and Information Science
harshrc [at] ccs [dot] neu [dot] edu
Office: West Village H room 316
- Verification, Interactive theorem proving using ACL2, Mathematical Logic, Languages, History...
- I work with Pete Manolios.
- Brief intro:
- I graduated from IIT Kanpur(India) in 2002 with a degree in Electrical Engineering and worked as a Software Engineer for many years in Bangalore(India).
I maintain ACL2s, which is a eclipse-based graphical user-interface to ACL2 Theorem Prover and more.
ACL2s was developed by Peter Dillinger and features extensions to ACL2 by Daron Vroon, Pete Manolios and myself that make theorem-proving easily accessible to beginners.
Publications and Reports
Integrating Testing and Interactive Theorem Proving [link]
with Peter Dillinger, Matt Kaufmann and Pete Manolios. ACL2 2011
Automated Specification Analysis using an Interactive Theorem Prover (revised version)[pdf]
with Pete Manolios. FMCAD 2011
- Edsger W. Dijkstra's manuscripts. Always makes for great reading!
- How to prove theorems formally - Kaufmann and Moore
- A good proof is a proof that makes us wiser! - Y. Manin
- Quick Latex Notes by Jeremy Osterhouse.
- Quickstart HTML guide by Charles Kelly.
- Quickstart Emacs Lisp tutorial by Bastien Guerry
- Quickstart svn version control tutorial
- Steve Bourne's original shell tutorial
Computer-Aided Reasoning lab:
| Eugene G
| Vasilis P
| Mitesh J
| Jaideep R
My Delecious bookmarks
| Watch Football!!
| On my name
Law of Excluded Middle