Estrin Family Professor of Computer Science
My field of research concerns the application of formal (mathematical) methods to the specification, verification, systematic development, and automatic synthesis of reactive, real-time, and hybrid computerized systems.
The mission of formal methods is to guarantee, using mathematical and logical techniques, that constructed systems (and programs) are correct, reliable, and absolutely error-free. My work so far has concentrated on the use of temporal logic, and its appropriate extensions for real time and hybrid systems, as a convenient specification language, and the development of deductive and algorithmic (model checking) techniques for verifying that a given system satisfies its specification.
My current activities in this general area involve the application and enhancements of deductive verification methods to hardware designs such as the out-of-order execution component of modern micro-process chips, tools and methods for verifying the correctness of translators from a high-level specification into a running code, the development of methods for symbolic model checking of parameterized systems, and general techniques for using abstraction and composition as part of the verification process, enabling the handling of very large designs and systems.
- [with Y. Kesten] A Compositional Approach to CTL* Verification. Theoretical Computer Science. Elsevier, to appear, 2004.
- [with Y. Fang, N. Piterman, and L. Zuck] Liveness with incomprehensible ranking. In 10th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 2988, Springer-Verlag, Barcelona, Spain, March 2004, pp. 482-496
- [with T. Arons] TLPVS : A PVS-based LTL verification system. In N. Dershowitz (editor), Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of his 64th Birthday, Lecture Notes in Computer Science 2772, Springer-Verlag, 2004, pp. 598-625.