Teaching

Classroom Teaching

During Fall'17 I was a Teaching Assistant for 15-122 Principles of Imperative Programming, Carnegie Mellon's introductory imperative programming course. I taught two recitation periods, a lab period, held office hours, participated in grading, helped draft exams, and served as a liason between the two instructors and approximately two dozen undergraduate Teaching Assistants.

I was a Teaching Assistant for the Spring'16 iteration of 15-424 Foundations of Cyber-Physical Systems at Carnegie Mellon. In addition to holding weekly recitations and grading assignments, I transitioned course infrastructure to the use of the KeYmaera X theorem prover and re-designed several recitations to support this transition. Using KeYmaera X instead of the legacy KeYmaera 3 system enabled students to take on more ambitious course projects. These projects were presented to judges from industry, government, and academia at a competition shortly after the course completed.

I re-designed and presented a guest lecture in Carnegie Mellon's Spring'17 iteration of 15-424 and guest lectured on numerous occastions in Carnegie Mellon's imperative programming course (15-122).

Undergraduate Advising

Undergraduate research is a fantastic pedagogical tool for teaching problem solving, research, and communication skills. I've mentored many undergraduate research projects, some of which resulted in undergraduate theses or peer-reviewed publications:

• May Wu (MIT '20), Verification of Magnetic Control Algorithms for Fusion Reactors. Publication in FMICS.
• Viren Bajaj (CMU ’18) and Karim Elmaaroufi (CMU ’17), Verification of SCUBA Ascent Protocols. Publication in EMSOFT.
• David Bayani (CMU ’16), Undergraduate thesis: Investigation and Implementation of Invariant Generation in The KeYmaera System for Hybrid Dynamical Systems.

Software

Software can play a key role in helping students explore concepts. I've developed several pieces of software that instructors at various universities have incorporated into their teaching.

• The KeYmaera X theorem prover plays a central role in Carnegie Mellon's Cyber-Physical Systems course, and has been used in more limited capacity in courses on Cyber-Physical Systems at other universities, as well as in tutorials and summer schools.
• A simple demo of adaptive cruise control is useful for teaching the role that constraints play in safe reinforcement learning.
• The KeYmaera I theorem prover was developed to support Carnegie Mellon's Constructive Logic course, an undergraduate offering in Carengie Mellon's Computer Science Department.
• A simple discrete predator/prey model was used in a Math Bio course at the University of Pittsburgh's Mathematics department.

Other Teaching Experience

• I designed and taught CS-themed weekly enrichment activities at Pittsburgh Public School's Science and Technology magnet.
• I developed pedagogical software for 15-317 Constructive Logic at Carnegie Mellon. I also provided some support for both course staff and students in both 15-317 and the Spring'17 iteration of 15-424.
• As an undergraduate, I tutored throughout the Computer Science curriculum and served as a Supplemental Instructor for an undergraduate Computer Organization course at Carthage College, a small liberal arts college.