Peter C. Dillinger Computer Science Ph.D. Student Northeastern University Office: West Village H room 330 plcld:@:ccs:.:neu:.:edu

Work

ACL2 theorem prover

Papers:

• Peter C. Dillinger, Panagiotis Manolios, J Moore, and Daron Vroon.
  ACL2s: "The ACL2 Sedan".
  Proceedings of the 7th Workshop on User Interfaces for Theorem Proving, Electronic Notes in Theoretical Computer Science 174(2), pages 3-18, Elsevier, 2007. (UITP, part of FLoC'06)
  (Another version presented as a demo at ICSE 2007.)

• Peter C. Dillinger, Matt Kaufmann, and Panagiotis Manolios.
  Hacking and Extending ACL2.
  Presented at the 7th Workshop on the ACL2 Theorem Prover and its Applications (2007). (Refereed but published online only.)

The tool:

• ACL2s: "The ACL2 Sedan", a rich user interface for the award-winning ACL2 theorem proving system in Eclipse. My interface has been used successfully in several graduate courses and one large undergraduate course.

Data structures in verification

Publications:

• Peter C. Dillinger and Panagiotis Manolios.
  Fast, All-Purpose State Storage.
  (To appear) 16th International SPIN Workshop on Model Checking Software (SPIN), 2009.

• Peter C. Dillinger and Panagiotis Manolios.
  Bloom Filters in Probabilistic Verification.
  Formal Methods in Computer-Aided Design (FMCAD), 2004.

• Peter C. Dillinger and Panagiotis Manolios.
  Fast and Accurate Bitstate Verification for SPIN.
  11th International SPIN Workshop on Model Checking Software (SPIN), 2004.

• Peter C. Dillinger and Panagiotis Manolios.
  Enhanced Probabilistic Verification with 3Spin and 3Murphi.
  12th International SPIN Workshop (SPIN), 2005. (Tool paper.)

Tools:

• 3SPIN ("Triple Spin"), a modified version of the SPIN model checker with enhancements to approximate state storage.

• 3Murphi ("Triple Murphi"), a modified version of the Murphi verifier with enhancements to approximate state storage.

Resume/CV

I am looking for a job to start this fall. Here is my resume/CV.

Summer Gigs

• 2004 - Intern at the NASA/JPL Laboratory for Reliable Software with Gerard Holzmann and Rajeev Joshi.
• 2005, 2007 - Math instructor for the Georgia Governor's Honors Program, teaching Cryptography, Logic, and Programming.
• 2006 - Intern with the NASA/Ames Automated Software Engineering group, working on Java PathFinder with Willem Visser, Peter Mehlitz, and Corina Pasareanu.

Teaching