Senior Research Associate
My primary research interest is the application of automated deduction to program synthesis, verification, and optimization. My current research aims at developing a logical programming environment for the construction of reliable and efficient distributed systems. In cooperation
with the Nuprl and Ensemble research groups I have built semantics-based formal tools that can automatically optimize protocol stacks of the Ensemble group communication system. The tools create a fast-path through a stack of communication protocols for common sequences of operation, reconfigure the system’s code accordingly, and give a Nuprl proof of the correctness of the optimizations. The optimized code is tested to perform two to three times faster than the original one.
I am also interested in the development of automatic proof procedures for classical and non-classical logics. Together with former students from the Technical University of Darmstadt I work on proof search methods based on matrix-characterizations of logical validity, a very compact representation of the search space. We have developed a uniform proof search procedure for classical logic, intuitionistic logic, various modal logics, and fragments of linear logic. We have also developed a uniform algorithm for transforming the machine-found matrix proofs into sequent proofs, which enables us to guide the development of proofs in interactive assistants such as Nuprl. In the past year we have integrated the matrix-based proof procedure into the Nuprl proof development system, extended its theoretical foundations to the multiplicative exponential fragment of linear logic, and developed a matrix-based proof method for inductive specification proofs.
Program Committee Member: 1st International Conference on Computational Logic, Automated Deduction Stream; International Workshop FroCoS’2000; CADE-17 Workshop on the Automation of Proof by Mathematical Induction.
Review Panel Member: NSF Information Technology Research, Software; NSF Information Technology Research, Verification.
Referee: Journal of Symbolic Computation; CSL 2000.
“Automating Inductive Specification Proofs.” Fundamenta Informatica, 39 (1-2) (1999), 181–209 (with B. Pientka).
“Building Reliable, High-Performance Systems from Components.” Proc. 17th ACM Symposium on Operating System Principles (SOSP’99), Operating Systems Review 34(5) (December 1999), 80–92 (with X. Liu, R. van Renesse, J. Hickey, M. Hayden, K. Birman, and R. Constable).
“The Horus and Ensemble Projects: Accomplishments and Limitations.” Proc. DISCEX’00 (January 2000), 149-161 (with K. Birman, B. Constable, M. Hayden, J. Hickey, R. van Renesse, O. Rodeh, and W. Vogels).
“Matrix-based Constructive Theorem Proving.” Intellectics and Computational Logic. Papers in honor of Wolfgang Bibel, Applied Logic Series 19, Kluwer (April 2000) (with J. Otten, S. Schmitt, and B. Pientka).
“The Nuprl Open Logical Environment.” Proc. 17th International Conference on Automated Deduction, LNAI 1831, Springer (June 2000) (with S. Allen, R. Constable, R. Eaton, and L. Lorigo).