Reseach
Interest |
I am interested in developing tools and techniques that aid in the development
of correct, reliable software systems. With a breadth of knowledge in
analysis, verification, languages, and compilers, I have focused on improving
formal verification algorithms and tools--so that these might become equally as
capable as they are essential to the production of complex, reliable software.
|
| Education |
All: Georgia Institute of Technology, Atlanta, GA
| 8/2003 - Present |
Doctor of Philosophy in Computer Science (in progress)
Research: Algorithms and data structures for explicit-state model checking
|
| 8/2002 - 8/2003 |
Master of Science in Computer Science
Areas of focus: Compilers, Languages, Program Analysis and Verification, and Formal Methods
|
| 8/1999 - 8/2002 |
Bachelor of Science in Computer Science
Specialization areas: Compilers, Operating Systems, Artificial Intelligence, Theory
|
|
Work
Experience |
Research assistant · Georgia Tech College of Computing
| 1/2005 - 5/2007 |
Research with Prof. Manolios on an NSF project to make the ACL2 theorem
proving system more accessible to beginners, so that it could be introduced
in undergraduate courses. The current tool is available as a plug-in to
Eclipse called "ACL2s: The ACL2 Sedan"; it has been used quite successfully
in several graduate courses.
|
| 8/2004 - 12/2004, 5/2003 - 5/2004, 5/2001 - 8/2001 |
Other projects with Prof. Manolios and Prof. Harrold.
|
Industry Research Intern · NASA Ames Laboratory/Mission Critical Technologies
| 5/2004 - 7/2004 |
Summer intern with the Robust Software Engineering group, working with
Willem Visser, Corina Pasareanu, and Peter Mehlitz. I made some significant
advancements to the Java PathFinder (JPF) model checker. Most notably, 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.
|
Instructor · Georgia Governor's Honors Program
| 6/2005 - 7/2005, 6/2007 - 7/2007 |
Math instructor for the six week program, which gives enrichment in
mathematics to about a hundred of the state's most talented, most interested
high school juniors and seniors.
- Developed my own curricula for courses based on Math that is not
offered in high schools.
- Gave daily lectures and supervised student research projects.
- Taught courses on Cryptography, Logic, Theory of Computation,
Functional Programming, and Introductory Programming.
|
Industry Research Intern · NASA/Caltech Jet Propulsion Laboratory
| 5/2004 - 7/2004 |
Summer intern at the Laboratory for Reliable Software, working with
Gerard Holzmann and Rajeev Joshi.
- Integrated some of my enhancements to the SPIN model checker into an
official release.
- Worked on specification and implementation of automaton-based static
checkers.
- Developed a unique preprocessor for C that supports program analysis.
|
Teaching assistant · Georgia Tech College of Computing
| 8/2002 - 5/2003 (Graduate), 5/2000 - 5/2002 (Undergraduate) |
Assisted in undergraduate Computer Science courses by giving recitations,
providing one-on-one help, grading work, and developing entire tests and
programming assignments.
|
|
| Publications |
- Peter C. Dillinger and Panagiotis Manolios.
Enhanced Probabilistic Verification with 3Spin and 3Murphi.
Tool paper in proc. of 12th International SPIN Workshop (2005).
Volume 3639 of Springer LNCS.
Peter C. Dillinger and Panagiotis Manolios.
Bloom Filters in Probabilistic Verification.
In Proc. of Formal Methods in Computer-Aided Design (FMCAD), 2004.
Volume 3312 of Springer LNCS.
Peter C. Dillinger and Panagiotis Manolios.
Fast and Accurate Bitstate Verification for SPIN.
In Proc. of 11th International SPIN Workshop (2004).
Volume 2989 of Springer LNCS.
|
| Honors |
|
| References |
- Panagiotis (Pete) Manolios, Assistant Professor
manolios@cc.gatech.edu
404-894-9219
- Mary Jean Harrold, Professor
harrold@cc.gatech.edu
404-385-0612
- More references available upon request.
|