Home

This web site described the work realized under grant NSF ITR: Little Engines of Proof #0326540 (2003-2007). The grant was awarded to Drs. Natarajan Shankar(PI), Harald Ruess (Co-PI), Ashish Tiwari (Co-PI) (Stanford Research Insitute, SRI), Christopher Lynch (Co-PI) (Clarkson University) and Christelle Scharff (Co-PI) (Pace University).

• Pace University participants:

  • Dr. Christelle Scharff cscharff@pace.edu

  • Michael Rehse (Undergraduate student)

  • Sokharith Sok (Former graduate student)

• Contributions:

  • Building Bridges. Mini-Workshop on Automated Deduction, Formal Digital Libraries and Little Engines of Proof, Stanford Research Institute, Palo Alto, October 2003 [slides]

  • On the Combination of Congruence Closure and Completion. International Conference on Artificial Intelligence and Symbolic Computation (AISC), Linz, Austria, 2004 (joint work with Dr. Leo Bachmair) [paper,slides,bibtex]

  • Little Engines of Proof: Progress Report and Future. Little Engines of Proof/Logosphere Meeting, Carnegie Mellon University, Pittsburgh, January 2006 [slides]

  • From Design by Contract to Static Analysis of Java Programs: A Teaching Approach. International Formal Methods Education Workshop (FMEd), Hamilton, Canada, 2006 (joint work with Sokharith Sok) [paper,slides]

  • A Graph-Based Approach to Build Extended Canonizers. International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), Phnom Penh, Cambodia, 2006 (short paper) (joint work with Dr. Silvio Ranise) [slides,bibtex]

  • Building Extended Canonizers by Graph-Based Deduction. International Colloquium on Theoretical Aspects of Computing (ICTAC), Macao SAR, China, 2007 (joint work with Dr. Silvio Ranise) [paper,slides,bibtex]

• Master Thesis:

  • Java and Web Extensions of the Yices Little Engine of Proof. Sokharith Sok. December, 2006 [manuscript,slides]