Tim Teitelbaum
Associate Professor
tt@cs.cornell.edu
http://www.cs.cornell.edu/Info/People/tt/Tim_Teitelbaum.html
PhD Carnegie-Mellon University, 1975
My research is concerned with the use of fine-grain dependence graphs for specification, development, and analysis of software and hardware systems. The objective is a new generation of tools that provide far more precise and
complete information about the structure of complex
systems. I am working to improve the
performance and functionality of generic dependence-graph technology, and am also exploring the use of the technology in various application domains. |
|
Dependence-graph technology can be used in a program understanding system, where the graphs may include forward and backward links between each assignment statement and possible uses of the values stored by that assignment. Pointer analysis can be used so that indirect loads and stores through pointers are taken into account, as well as indirect function calls.
Dataflow analysis can be used so that links between unrelated assignments and uses are
excluded. Operations that highlight forward and backward slices show the impact of a given statement on the rest of the program (forward slicing), and the impact of the rest of a program on a given statement (backward slicing). Operations that highlight paths between nodes in the dependence graph (chops) show ways in which the program points are interdependent (or
independent). Uses of slicing and chopping include software development, maintenance and re-engineering of legacy code, test-data generation, security-assurance and
safety-assurance inspection, and semantic interference checking in configuration management systems.
I am working with Ph.D. student Lyn Millett, who is studying program dependence-graphs and slicing of concurrent programs.
I am also working with T. Reps of the University of Wisconsin and E. Clarke and S. Shankar of CMU to understand how slicing can be used to abstract VHDL and Verilog hardware designs
for the purpose of improving the performance of simulation and formal
verification.
University Activities
Professional Activities
-
Co-founder and Chairman:
GrammaTech, Inc.
Lectures
-
Static-semantic analysis based
on dependence graphs. Sandia
National Laboratory,
Albuquerque, NM, Apr. 1999.
-
—. Northrop-Grumman, Pico
Rivera, CA, Apr. 1999.
-
—. National Security Agency,
Linthicum Heights, MD, Jan.
1999.
- —. NCC, Bowie, MD, Jan.
1999.
Publications
-
Issues in Slicing Promela and its
Applications to Protocol Understanding and Analysis.
International Journal on
Software Tools and
Technology Transfer, to
appear (with L. I. Millett).
-
Channel Dependence Analysisfor Slicing Promela.
Proceedings of the International Symposium on
Software Engineering for
Parallel and Distributed
Systems (PDSE 99) (May,
1999), 52-61 (with L. I. Millett).
-
Slicing Promela and its
Applications to Model
Checking, Simulation, and
Protocol Understanding.
Proceedings of the 4th
Workshop on Automata
Theoretic Verification with
the SPIN Model Checker
(SPIN 98) (Nov 1998), 75-83
(with L. I. Millett).
|