1998 - 1999 CS Annual Report                                                                  Faculty
choices.gif (4488 bytes)
 

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. 

tim.tif (84338 bytes)

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 

  • On leave spring 1999 

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).