| Objective |
I am looking for a career in which I can apply and expand the science of
software. I have made important contributions to tools for software analysis
and reasoning, but my interests include almost every aspect of developing
correct, efficient, robust, and secure systems.
|
| Education |
Doctor of Philosophy in Computer Science (anticipated graduation: Fall 2009)
Northeastern University, 2007 - present; Georgia Institute of Technology, 2003 - 2007
Data Structures in Explicit-State Model Checking (thesis research):
I made some improvements to known probabilistic state storage
techniques in explicit-state model checkers such as Spin and Mur&phi,
but those techniques still require infeasible foresight to make best use of
available memory.
I demonstrate a new alternative that is uniquely adaptive but also fast.
The possibility of overlooking an error is never far from the theoretical
minimum (for available memory and this class of solution), yet it is
faster than popular alternatives when using multiple processor cores.
ACL2s: "The ACL2 Sedan" (assistantship research):
I am the primary developer of ACL2s, an Eclipse-based development
environment for the award-winning ACL2 theorem proving system.
Developed under an NSF grant, ACL2s has enabled hundreds of students to
learn about logic and theorem proving without stumbling over a delicate
and esoteric interface.
I tackled significant technical barriers to providing an interface that is
simultaneously robust, permissive, and convenient.
Because of its unique features, ACL2s is my own favored interface to ACL2.
ACL2s is ~30K lines of Java and ~7K lines of ACL2 code.
Master of Science in Computer Science · Georgia Institute of Technology · 2002 - 2003
- Areas of focus: Compilers, Languages, Program Analysis and Verification, and Formal Methods
Bachelor of Science in Computer Science · Georgia Institute of Technology · 1999 - 2002
- Highest honors designation (3.70 / 4.00 GPA)
- Areas of focus: Compilers, Operating Systems, Artificial Intelligence, Theory
|
| Industry |
Research Intern · NASA Ames Research Center/Mission Critical Technologies · Summer 2006
Robust Software Engineering group, under Willem Visser, Corina Pasareanu, and Peter Mehlitz
- State Matching in Java PathFinder:
JPF is an explicit-state model checker for concurrent Java programs.
I retooled
the state hashing and matching system to be much faster and provide highly
configurable and customizable state abstractions. Along with
integrating this and other improvements, I gained a reputation for
being able to track down and isolate deep bugs in JPF itself.
Research Intern · NASA/Caltech Jet Propulsion Laboratory · Summer 2004
Laboratory for Reliable Software, under Gerard Holzmann and Rajeev Joshi
- Integrated some of my data structure enhancements into an official
release of the SPIN model checker.
- Worked on specification and implementation of automaton-based static
checkers.
- Developed a preprocessor for C that supports program analysis.
|
| Teaching |
Instructor of Record · Northeastern University · Fall 2008
CS U290: "Logic and Computation," a relatively new class introducing freshman
students to logic through the ACL2 programming language,
logic and theorem prover. Students use my ACL2s development environment.
- Developed all lectures, assignments, and tests, loosely based on
previous term.
- Wrote detailed lecture notes (online) to compensate for lack of a
well-targeted textbook.
- Added a basic graphics library and restricted, beginner-friendly
session mode to ACL2s.
Instructor · Georgia Governor's Honors Program · Summers 2005 & 2007
Math department, under Dennis Stewart and Dale Lyles
- Developed my own curricula for summer enrichment courses for
enthusiastic high school students. (The program is legally mandated not
to teach material offered in high school.)
- Gave daily lectures and supervised student research projects.
- Taught courses on Cryptography, Logic, Theory of Computation,
Functional Programming, and Introductory Programming.
Teaching assistant · Georgia Tech and Northeastern University · 2000 - 2003, 2008
- Responsibilities have included recitations, grading,
giving one-on-one help, and developing entire tests, programming assignments,
and written assignments.
|
Papers/
Publications |
Fast, All-Purpose State Storage.
Coauthor: Panagiotis Manolios.
In Proc. of 16th International SPIN Workshop, 2009.
To appear, Springer LNCS.
Hacking and Extending ACL2.
Coauthors: Matt Kaufmann and Panagiotis Manolios.
Presented at 7th Workshop on the ACL2 Theorem Prover and its Applications, 2007.
(Refereed but published online only.)
ACL2s: "The ACL2 Sedan".
Coauthors: Panagiotis Manolios, J Moore, and Daron Vroon.
In Proc. of 7th Workshop on User Interfaces for Theorem Proving (UITP), 2006.
Volume 174, Issue 2 of Elsevier ENTCS.
(Another version was a demo at ICSE 2007.)
Enhanced Probabilistic Verification with 3Spin and 3Murphi.
Coauthor: Panagiotis Manolios.
Tool paper in Proc. of 12th International SPIN Workshop, 2005.
Volume 3639 of Springer LNCS.
Bloom Filters in Probabilistic Verification.
Coauthor: Panagiotis Manolios.
In Proc. of Formal Methods in Computer-Aided Design (FMCAD), 2004.
Volume 3312 of Springer LNCS.
- Fast and Accurate Bitstate Verification for SPIN.
Coauthor: Panagiotis Manolios.
In Proc. of 11th International SPIN Workshop, 2004.
Volume 2989 of Springer LNCS.
|
| References |
- Panagiotis (Pete) Manolios, Associate Professor, Northeastern University
(My advisor for Master's and Ph.D.)
pete@ccs.neu.edu
+1 617 373 3694
- Willem Visser, Professor, Stellenbosch University
(My supervisor at NASA/Ames, where he was a contractor for many years)
willem@gmail.com
+27 (0)21 808 4232 (South Africa)
- Matt Kaufmann, Senior Research Scientist, University of Texas at Austin
(Collaborator and lead maintainer of ACL2)
kaufmann@cs.utexas.edu
+1 512 471 9780
- More references available upon request.
|
Other
Information |
- Interested in starting new employment around September
- Able to relocate
- U.S. Citizen
|