Thomas W. Reps Professor Computer Sciences Department University of Wisconsin-Madison 1210 West Dayton Street Madison, WI 53706-1685 USA

Contact Information:

E-mail: reps at cs.wisc.edu
Telephone: (608) 262-2091
Secretary: (608) 262-6616
Department: (608) 262-1204
Fax: (608) 262-9777
Finger information

Some Maps: Campus Map | Campus-to-Capitol Map | City Map

Ph.D., Cornell University, 1982 (CV, Biography, Research Summary, Past Research)

Research Interests:

• Program slicing, differencing, and merging
• Interprocedural dataflow analysis
• Alias analysis, pointer analysis, and shape analysis
• Other program-analysis problems
• Path problems
• Model checking
• Computer security
• Code instrumentation
• Computational differentiation and computational divided differencing
• Language-based program-development environments
• Incremental computing
• Attribute grammars
• Miscellaneous

See also Citeseer, Google Scholar, and DB&LP;.

Projects:

• Wisconsin Program-Slicing Project
• Wisconsin Safety Analyzer Project
• CMU-UW Software Model Checking Project

The tools that we are developing are based on static analysis: static analysis concerns techniques for obtaining information about the possible states that a program passes through during execution, without actually running the program on specific inputs. Instead, static-analysis techniques explore a program's behavior for all possible inputs and all possible states that the program can reach. To make this feasible, the program is ``run in the aggregate''---i.e., on abstract descriptors that represent collections of many states.

Most of our effort is focused on three topics:

• Static program analysis via 3-valued logic
• Static analysis of executables
• Weighted pushdown systems

The aim of this work [SRW02, RSW04] has been to create a parametric framework for program analysis that is capable of expressing rich properties of memory configurations, and confirming such behavioral properties as

• when the input to a list-insert program is an acyclic list, the output is an acyclic list, and
• when the input to a list-reversal program that uses destructive-update operations is an acyclic list, the output is an acyclic list.

This work was originally motivated by the problem of shape analysis for programs written in languages that permit destructive updating of dynamically allocated storage. The aim of shape analysis is to discover information (in a conservative way) about the possible ``shapes'' of the dynamically allocated data structures to which a program's pointer variables can point. As we investigated this problems more deeply, we discovered methods that allowed us to deal with properties of memory configurations other than just pure shape properties. For instance, recent work has concerned numeric properties [GDDRS04].

The key aspect of our approach is the way in which it makes use of 2-valued and 3-valued logic: 2-valued and 3-valued logical structures---i.e., collections of relations---are used to represent concrete and abstract stores, respectively; individuals represent entities such as memory cells, threads, locks, etc.; unary and binary relations encode the contents of variables, pointer-valued structure fields, and other aspects of memory states; and first-order formulas with transitive closure are used to specify properties such as sharing, cyclicity, reachability, etc. Formulas are also used to specify how the store is affected by the execution of the different kinds of statements in the programming language.

The analysis framework can be instantiated in different ways by varying the relation symbols of the logic, and, in particular, by varying which of the unary relations control how nodes are folded together. The specified set of relations determines the set of properties that will be tracked, and consequently what properties of stores can be discovered to hold at different points in the program by the corresponding instance of the analysis.

As a methodology for verifying properties of programs, the advantages of the 3-valued-logic approach are:

1. No loop invariants are required.
2. No theorem provers are involved, and thus every abstract execution step must terminate.
3. The method is based on abstract interpretation and satisfies conditions that guarantee that the entire process always terminates.
4. The method applies to programs that manipulate pointers and heap-allocated data structures.
5. The method eliminates the need for the user to write the usual proofs required with abstract interpretation---i.e., to demonstrate that the abstract descriptors that the analyzer manipulates correctly model the actual heap-allocated data structures that the program manipulates.

A prototype implementation that implements this approach has been created, called TVLA (Three-Valued-Logic Analyzer).

Static Analysis of Executables

The aim of this research is to recover intermediate representations that are similar to those that can be created for a program written in a high-level language. Our initial work has concerned x86 executables. The goal is to provide a platform that an analyst can use to understand the workings of potentially malicious code, such as COTS components, plugins, mobile code, worms, Trojans, and virus-infected code. In this context, the major challenge is that we must assume that the executable is untrustworthy, and hence symbol-table and debugging information cannot be relied upon (even if it is present). Instead, an analysis---called value-set analysis (VSA)---is carried out to recover information about the contents of memory locations and how they are manipulated by the executable [BR04].

A key feature of VSA is that it tracks address-valued and integer-valued quantities simultaneously. VSA is related to pointer-analysis algorithms that have been developed for programs written in high-level languages, which determine an over-approximation of the set of variables whose addresses each pointer variable can hold:

VSA determines an over-approximation of the set of addresses that each data object can hold at each program point.

VSA determines an over-approximation of the set of integer values that each data object can hold at each program point.

Value-set analysis has been incorporated into a tool called CodeSurfer/x86. The facilities of CodeSurfer/x86 provide an analyst with a powerful and flexible platform for investigating the properties and behaviors of an x86 executable, using either (i) CodeSurfer/x86's GUI, (ii) CodeSurfer/x86's scripting language, which provides access to all of the intermediate representations that CodeSurfer/x86 builds for the executable, or (iii) GrammaTech's Path Inspector, which is a tool that uses a sophisticated pattern-matching engine to answer questions about the flow of execution in a program.

CodeSurfer/x86 is the outcome of a joint project between the Univ. of Wisconsin and GrammaTech, Inc. CodeSurfer/x86 makes use of both IDAPro, a disassembly toolkit, and GrammaTech's CodeSurfer system, a toolkit for building program-analysis and inspection tools.

CodeSurfer/x86 is a tool for code understanding and code inspection that supports both a graphical user interface (GUI) and a scripting language for accessing a program's system dependence graph (SDG) [HRB90], as well as other information stored in CodeSurfer's intermediate representations (IRs). The GUI supports browsing (``surfing'') of an SDG, along with a variety of operations for making queries about the SDG---such as slicing [HRB90] and chopping [RR95]. The GUI allows a user to navigate through a program's source code using these dependences in a manner analogous to navigating the World Wide Web.

CodeSurfer's scripting language provides a programmatic interface to these operations, as well as to lower-level information, such as the individual nodes and edges of the program's SDG, call graph, and control-flow graph, and a node's sets of used, killed, and possibly-killed variables. By writing programs that traverse CodeSurfer's IRs to implement additional program analyses, the scripting language can be used to extend CodeSurfer's capabilities.

Weighted Pushdown Systems and their Application to Interprocedural Dataflow Analysis

This work has established new connections between interprocedural dataflow analysis and model checking of pushdown systems (PDSs). Various connections between dataflow analysis and model checking have been established in past work, e.g., [S91, S93, S98, EK99, CC00]; however, with one exception ([EK99]), past work has shed light only on the relationship between model checking and bit-vector dataflow-analysis problems, such as live-variable analysis and partial-redundancy elimination. In contrast, the results obtained in our work [RSJ03, RSJM] apply to (i) bit-vector problems, (ii) the one non-bit-vector problem addressed in [EK99], as well as (iii) certain dataflow-analysis problems that cannot be expressed as bit-vector problems, such as linear constant propagation SRH96 and affine-relation analysis MOS04. In general, the approach can be applied to any distributive dataflow-analysis problem for which the domain of transfer functions has no infinite descending chains. (Safe solutions are also obtained for problems that are monotonic but not distributive.)

The contributions of the work can be summarized as follows:

• Conventional dataflow-analysis algorithms merge together the values for all states associated with the same program point, regardless of the states' calling context. With the dataflow-analysis algorithm obtained via weighted PDSs, dataflow queries can be posed with respect to a regular language of stack configurations. Conventional merged dataflow information can also be obtained by issuing appropriate queries; thus, the new approach provides a strictly richer framework for interprocedural dataflow analysis than is provided by conventional interprocedural dataflow-analysis algorithms.
• Because the algorithm for solving path problems in weighted PDSs can provide a witness set of paths, it is possible to provide an explanation of why the answer to a dataflow query has the value reported.

The algorithms described in [RSJ03, RSJM] have been implemented in two libraries that solve reachability problems on weighted PDSs: WPDS and WPDS++ (available soon). These libraries have been used to create prototype implementations of context-sensitive interprocedural dataflow analyses for uninitialized variables, live variables, linear constant propagation, and the detection of affine relationships.

[Back to the top]

Recent Items of Note

Recent Papers

• ``Simulating reachability using first-order logic with applications to verification of linked data structures''
• ``Model checking x86 executables with CodeSurfer/x86 and WPDS++''
• ``Extended weighted pushdown systems''
• ``Abstraction refinement via inductive learning''
• ``On the utility of canonical abstraction''
• ``Weighted pushdown systems and their application to interprocedural dataflow analysis''
• ``CodeSurfer/x86 -- A platform for analyzing x86 executables''
• ``Automatic discovery of API-level exploits''
• ``Numeric analysis of array operations''
• ``A semantics for procedure local heaps and its abstractions''
• ``The boundary between decidability and undecidability for transitive closure logics''
• ``A relational approach to interprocedural shape analysis''
• ``Static program analysis via 3-valued logic''
• ``Verification via structure simulation''
• ``Analyzing memory accesses in x86 executables''
• ``Symbolically computing most-precise abstract operations for shape analysis''
• ``Numeric domains with summarized dimensions''
• ``Symbolic implementation of the best transformer''
• ``Model checking SPKI/SDSI''
• ``Design and implementation of a fine-grained software inspection tool''
• ``Computational divided differencing and divided-difference arithmetics''

[Back to the top]

Miscellaneous

The paper

• Horwitz, S., Reps, T., and Binkley, D., Interprocedural slicing using dependence graphs. In Proceedings of the ACM SIGPLAN 88 Conference on Programming Language Design and Implementation, (Atlanta, GA, June 22-24, 1988), ACM SIGPLAN Notices 23, 7 (July 1988), pp. 35-46. [abstract]

• Horwitz, S., Reps, T., and Binkley, D., Interprocedural slicing using dependence graphs. 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation (1979 - 1999): A Selection, K.S. McKinley, ed., ACM SIGPLAN Notices 39, 4 (April 2004), 232-243.

A retrospective on the paper was published as

• Horwitz, S., Reps, T., and Binkley, D., Retrospective: Interprocedural slicing using dependence graphs. 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation (1979 - 1999): A Selection, K.S. McKinley, ed., ACM SIGPLAN Notices 39, 4 (April 2004), 229-231. [retrospective (PS); retrospective (PDF)]

An extended version of the PLDI 88 paper later appeared as the following journal paper:

• Horwitz, S., Reps, T., and Binkley, D., Interprocedural slicing using dependence graphs. ACM Transactions on Programming Languages and Systems 12, 1 (January 1990), 26-60. [abstract; paper]

[Back to the top]

Availability of Program-Slicing Tools

The Wisconsin Program-Slicing Tool

The The Wisconsin Program-Slicing Tool is a software system that supports operations on C programs, including backward slicing, forward slicing, and chopping [TOPLAS90, FSE94, FSE95b], which can help the user gain an understanding of what a program does and how it works. The Wisconsin Program-Slicing Tool consists of a package for building and manipulating control-flow graphs and program dependence graphs, as well as a front-end that parses C programs and translates them to the internal representations used for slicing.

• The Wisconsin Program-Slicing Tool
• ``The Wisconsin Program-Slicing Tool 1.0, Reference Manual''
• Man page for the batch version of the Wisconsin Program-Slicing Tool

Although the Wisconsin Program-Slicing Tool was distributed from 1996-2000 for not-for-profit research purposes under license from the University of Wisconsin, it is no longer being distributed. However, there is a commercial tool available, named CodeSurfer, that is derived from the Wisconsin implementation and is available from GrammaTech, Inc. GrammaTech has improved on the Wisconsin implementation considerably (both in terms of speed and space efficiency). GrammaTech also provides CodeSurfer to academic researchers on very favorable terms.

CodeSurfer

The Wisconsin program-slicing technology is now available in a commercial product, the CodeSurfer^tm tool available from GrammaTech, Inc.

CodeSurfer builds a dependence-graph program representation and provides a GUI for exploring this web. The dependence graph includes forward and backward links between each assignment statement and possible uses of the values stored by that assignment. Pointer analysis is used so that indirect loads and stores through pointers are taken into account, as well as indirect function calls. Dataflow analysis is 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) [TOPLAS90, FSE94]. Operations that highlight paths between nodes in the dependence graph (chops) show ways in which the program points are interdependent (or independent) [FSE95b]. CodeSurfer's scripting language, which provides access to the dependence-graph program representation and the Tk widget set, is used for extensibility and for batch applications.

Full information about CodeSurfer is available here, where you can find

• full documentation,
• whitepapers,
• pricing information,
• information about use by academic researchers,
• the site for downloading an evaluation copy.

• Language: C (full support), C++ (alpha support)
• Program length: < 200K SLOC

[Back to the top]

Categorized Index to Publications

Overview

• ``Program analysis via graph reachability'', IST
  (also ``Program analysis via graph reachability'', TR-1386, and
  ``Program analysis via graph reachability'', ILPS 97)
• ``The use of program dependence graphs in software engineering''

The Wisconsin Program-Slicing Tool

• The Wisconsin Program-Slicing Tool
• License for the Wisconsin Program-Slicing Tool
• ``The Wisconsin Program-Slicing Tool 1.0, Reference Manual''
• Man page for the batch version of the Wisconsin Program-Slicing Tool

CodeSurfer System

• Short description of the CodeSurfer system
• CodeSurfer^tm web page

Slicing

• ``Program specialization via program slicing''
• ``Speeding up slicing''
• ``Interprocedural slicing of computer programs using dependence graphs''
• ``Multi-procedure program integration''
• ``Efficient comparison of program slices''
• ``Interprocedural slicing using dependence graphs'', TOPLAS 1990
  (also ``Interprocedural slicing using dependence graphs'', PLDI 1988)

Chopping

• ``Precise interprocedural chopping''

Differencing

• ``Identifying semantic differences in programs with procedures''
• ``A new algorithm for semantics-based program integration''

Merging

• ``Program integration for languages with procedure calls''
• ``A program integration algorithm that accommodates semantics-preserving transformations'', TOSEM 1992
  (also ``A program integration algorithm that accommodates semantics-preserving transformations'', SIGSOFT 1990)
• ``Multi-procedure program integration''
• ``A new algorithm for semantics-based program integration''
• ``Illustrating interference in interfering versions of programs''
• ``Integrating non-interfering versions of programs'', TOPLAS 1989
  (also ``Integrating non-interfering versions of programs'', POPL 1988,
  ``Semantics-based program integration'', and
  ``Support for integrating program variants in an environment for programming in the large'')

Algebra of slices (and applications to program merging)

• ``New programs from old''
• ``Algebraic properties of program integration'', SCP 1991
  (also ``Algebraic properties of program integration'', ESOP 1990)
• ``A theory of program modifications''
• ``Modification algebras''

Semantics and slicing

• ``Semantics of program representation graphs''
• ``The semantics of program slicing and program integration''
• ``The multi-procedure equivalence theorem''
• ``On the adequacy of program dependence graphs for representing programs''

Other applications of slicing

• ``Program slicing of hardware description languages''
• ``Program slicing for design automation''
• ``Partial evaluation using dependence graphs''
• ``Program specialization via program slicing''
• ``Semantic foundations of binding-time analysis for imperative programs''

Implemented integration system (for a small Pascal subset)

• ``The Wisconsin Program-Integration System''
• ``The Wisconsin Program-Integration System Reference Manual: Release 2.0''
• ``Demonstration of a prototype tool for program integration''

Miscellaneous

• ``Undecidability of context-sensitive data-dependence analysis''
• ``Correctness of an algorithm for reconstituting a program from a dependence graph''

Ph.D. Dissertations

• ``Partial evaluation using dependence graphs''
• ``Multi-procedure program integration''
• ``A new algorithm for semantics-based program integration''
• ``Dependence-based representations for programs with reference variables''

[Back to the top]

Interprocedural Dataflow Analysis

Demand IDFA via bottom-up logic programming and the magic-sets transformation

• ``Demand interprocedural program analysis using logic databases''
  (also ``Solving demand versions of interprocedural analysis problems'')

Exhaustive and Demand IDFA via graph reachability

• ``Program analysis via graph reachability'', IST
  (also ``Program analysis via graph reachability'', TR-1386, and
  ``Program analysis via graph reachability'', ILPS 97)
• ``Demand interprocedural dataflow analysis'', TR-1283
  (also ``Demand interprocedural dataflow analysis'', FSE 1995)
• ``Precise interprocedural dataflow analysis via graph reachability''
• ``Interprocedural dataflow analysis via graph reachability''

IDFA using more than graph reachability

• ``Extended weighted pushdown systems''
• ``Weighted pushdown systems and their application to interprocedural dataflow analysis'', SCP
  (also ``Weighted pushdown systems and their application to interprocedural dataflow analysis'', SAS 2003)
• ``Precise interprocedural dataflow analysis with applications to constant propagation'', TCS 1996
  (also ``Precise interprocedural dataflow analysis with applications to constant propagation'', FASE 1995)

PTIME completeness of IDFA

• ``On the sequential nature of interprocedural program-analysis problems''

[Back to the top]

Alias Analysis, Pointer Analysis, and Shape Analysis

• ``Simulating reachability using first-order logic with applications to verification of linked data structures''
• ``Abstraction refinement via inductive learning''
• ``On the utility of canonical abstraction''
• ``Numeric analysis of array operations''
• ``A semantics for procedure local heaps and its abstractions''
• ``A relational approach to interprocedural shape analysis''
• ``Static program analysis via 3-valued logic''
• ``Verification via structure simulation''
• ``Symbolically computing most-precise abstract operations for shape analysis''
• ``Verifying temporal heap properties specified via evolution logic''
• ``Finite differencing of logical formulas for static analysis''
• ``Parametric shape analysis via 3-valued logic''
• ``Putting static analysis to work for verification: A case study''
• ``Shape analysis'', CC 2000
• ``Pointer analysis for programs with structures and casting''
• ``A decidable logic for describing linked data structures''
• ``Program analysis via graph reachability'', IST
  (also ``Program analysis via graph reachability'', TR-1386, and
  ``Program analysis via graph reachability'', ILPS 97)
• ``Program specialization via program slicing''
• ``Solving shape-analysis problems in languages with destructive updating'', TOPLAS
  (also ``Solving shape-analysis problems in languages with destructive updating'', POPL 1996, and
  ``Solving shape-analysis problems in languages with destructive updating'', TR-1276)
• ``Shape analysis as a generalized path problem''
• ``Dependence-based representations for programs with reference variables''
• ``Dependence analysis for pointer variables''

[Back to the top]

Other Program-Analysis Problems

• ``Numeric domains with summarized dimensions''
• ``Symbolic implementation of the best transformer''
• ``The interprocedural express-lane transformation''
• ``Interprocedural path profiling and the interprocedural express-lane transformation'', Melski thesis
• ``Typestate checking of machine code''
• ``Safety-checking of machine code'', Xu thesis
• ``Safety checking of machine code'', PLDI 00
• ``Putting static analysis to work for verification: A case study''
• ``Physical type checking for C'', PASTE 99
  (also ``Physical type checking for C'', BL0113590-990302-04)
• ``Coping with type casts in C'', FSE 99
  (also ``Coping with type casts in C'', BL0113590-990202-03)
• ``Interprocedural path profiling'', CC 99
  (also ``Interprocedural path profiling'', TR-1382)
• ``Techniques for software renovation''
• ``Program analysis via graph reachability'', IST
  (also ``Program analysis via graph reachability'', TR-1386, and
  ``Program analysis via graph reachability'', ILPS 97)
• ``Interconvertibility of a class of set constraints and context-free language reachability'', TCS
  (also ``Interconvertibility of set constraints and context-free language reachability'', PEPM 97)
• ``Identifying modules via concept analysis'', TSE
  (also ``Identifying modules via concept analysis'', ICSM 97)
• ``The use of program profiling for software maintenance with applications to the Year 2000 Problem''
  (also ``The use of program profiling in software testing'')
• ``Method of troubleshooting data-dependent anomalies in computer programs''
• ``BTA termination using CFL-reachability''
• ``Program generalization for software reuse: From C to C++''
• ``Semantic foundations of binding-time analysis for imperative programs''

Ph.D. Dissertations

• ``Safety-checking of machine code''
• ``Techniques for software renovation''
• ``Partial evaluation using dependence graphs''

[Back to the top]

Path Problems

• ``Model checking of unrestricted hierarchical state machines''
• ``Program analysis via graph reachability'', IST
  (also ``Program analysis via graph reachability'', TR-1386, and
  ``Program analysis via graph reachability'', ILPS 97)
• ``Interconvertibility of a class of set constraints and context-free language reachability'', TCS
  (also ``Interconvertibility of set constraints and context-free language reachability'', PEPM 97)
• ``Undecidability of context-sensitive data-dependence analysis''
• ``Speeding up slicing''
• ``Interprocedural slicing of computer programs using dependence graphs''
• ``Interprocedural slicing using dependence graphs'', TOPLAS 1990
  (also ``Interprocedural slicing using dependence graphs'', PLDI 1988)
• ``Demand interprocedural dataflow analysis'', TR-1283
  (also ``Demand interprocedural dataflow analysis'', FSE 1995)
• ``Precise interprocedural dataflow analysis via graph reachability''
• ``Interprocedural dataflow analysis via graph reachability''
• ``On the sequential nature of interprocedural program-analysis problems''
• ``Shape analysis as a generalized path problem''

Other Path Problems

• ``Extended weighted pushdown systems''
• ``Weighted pushdown systems and their application to interprocedural dataflow analysis'', SCP
  (also ``Weighted pushdown systems and their application to interprocedural dataflow analysis'', SAS 2003)
• ``The interprocedural express-lane transformation''
• ``On generalized authorization problems''
• ``An incremental algorithm for a generalization of the shortest-path problem''
• ``On the computational complexity of dynamic graph problems''
• ``An incremental algorithm for maintaining the dominator tree of a reducible flowgraph''
• ``Precise interprocedural dataflow analysis with applications to constant propagation'', TCS 1996
  (also ``Precise interprocedural dataflow analysis with applications to constant propagation'', FASE 1995)
• ``Interprocedural path profiling'', CC 99
  (also ``Interprocedural path profiling'', TR-1382)

Ph.D. Dissertations

• ``Interprocedural path profiling and the interprocedural express-lane transformation''
• ``Bounded Incremental Computation''
• ``Multi-procedure program integration''

[Back to the top]

Model Checking

• ``Model checking x86 executables with CodeSurfer/x86 and WPDS++''
• ``Extended weighted pushdown systems''
• ``Weighted pushdown systems and their application to interprocedural dataflow analysis''
• ``Automatic discovery of API-level exploits''
• ``Model checking SPKI/SDSI''
• ``Verifying temporal heap properties specified via evolution logic''
• ``On generalized authorization problems''
• ``Analysis of SPKI/SDSI certificates using model checking''
• ``Model checking of unrestricted hierarchical state machines''
• ``LTL model checking for systems with unbounded number of dynamically created threads and objects''

[Back to the top]

Computer Security

• ``Model checking x86 executables with CodeSurfer/x86 and WPDS++''
• ``CodeSurfer/x86 -- A platform for analyzing x86 executables''
• ``Automatic discovery of API-level exploits''
• ``Analyzing memory accesses in x86 executables''
• ``On generalized authorization problems''
• ``Model checking SPKI/SDSI''
• ``Typestate checking of machine code''
• ``Safety checking of machine code'', PLDI 00

Ph.D. Dissertations

• ``Safety-checking of machine code'', Xu thesis

[Back to the top]

Code Instrumentation

• ``The interprocedural express-lane transformation''
• ``Debugging via run-time type checking''
• ``Interprocedural path profiling'', CC 99
  (also ``Interprocedural path profiling'', TR-1382)
• New technology for Year 2000 Problem tools
• ``The use of program profiling for software maintenance with applications to the Year 2000 Problem''
  (also ``The use of program profiling in software testing'')

Ph.D. Dissertations

• ``Interprocedural path profiling and the interprocedural express-lane transformation'', Melski thesis

[Back to the top]

Computational Differentiation and Computational Divided Differencing

• ``Algorithmic differencing''
• ``Computational divided differencing and divided-difference arithmetics''

[Back to the top]

Language-Based Program-Development Environments

• ``Programming environments''
• ``The Synthesizer Generator: A System for Constructing Language-Based Editors''
• ``The Synthesizer Generator Reference Manual: Third Edition''
• ``Language processing in program editors''
• ``Remote attribute updating for language-based editors''
• ``The Synthesizer Generator'', 1985 system
• ``The Synthesizer Generator'', PSDE 1984
• ``Incremental context-dependent analysis for language-based editors''
  (also ``Optimal-time incremental semantic analysis for syntax-directed editors'' and
  ``Incremental evaluation for attribute grammars with application to syntax-directed editors'')
• ``Static-semantic analysis in language-based editors''
• ``The Cornell Program Synthesizer: A syntax-directed programming environment''
• ``The why and wherefore of the Cornell Program Synthesizer''
• ``The Cornell Program Synthesizer''

Ph.D. Dissertations

• ``Techniques for software renovation''
• ``Generating Language-Based Environments''

[Back to the top]

Incremental Computing

• ``Finite differencing of logical formulas for static analysis''
• ``An incremental algorithm for a generalization of the shortest-path problem''
• ``On the computational complexity of dynamic graph problems''
• ``On competitive on-line algorithms for the dynamic priority-ordering problem''
• ``Incremental computation and dynamic algorithms''
• ``An incremental algorithm for maintaining the dominator tree of a reducible flowgraph''
• ``A categorized bibliography on incremental computation''
• ``Incremental computation''
• ``The Synthesizer Generator: A System for Constructing Language-Based Editors''
• ``Incremental evaluation for attribute grammars with unrestricted movement between tree modifications''
• ``Language processing in program editors''
• ``Remote attribute updating for language-based editors''
• ``The Synthesizer Generator'', 1985 system
• ``Incremental context-dependent analysis for language-based editors''
  (also ``Optimal-time incremental semantic analysis for syntax-directed editors'' and
  ``Incremental evaluation for attribute grammars with application to syntax-directed editors'')

Ph.D. Dissertations

• ``Bounded Incremental Computation''
• ``Generating Language-Based Environments''

[Back to the top]

Attribute Grammars

• ``Scan grammars: Parallel attribute evaluation via data-parallelism''
• ``The Synthesizer Generator: A System for Constructing Language-Based Editors''
• ``The Synthesizer Generator Reference Manual: Third Edition''
• ``Incremental evaluation for attribute grammars with unrestricted movement between tree modifications''
• ``Sublinear-space evaluation algorithms for attribute grammars''
• ``Remote attribute updating for language-based editors''
• ``The Synthesizer Generator'', 1985 system
• ``The Synthesizer Generator'', PSDE 1984
• ``Interactive proof checking''
• ``Incremental context-dependent analysis for language-based editors''
  (also ``Optimal-time incremental semantic analysis for syntax-directed editors'' and
  ``Incremental evaluation for attribute grammars with application to syntax-directed editors'')
• ``Static-semantic analysis in language-based editors''

Ph.D. Dissertations

• ``Generating Language-Based Environments''

[Back to the top]

Miscellaneous

• ```Maximal-munch' tokenization in linear time''

[Back to the top]

Please note that the definitive versions of these papers are the published versions. The PostScript versions are provided here as a courtesy, and, in some cases, there may be differences between the PostScript provided here and the published version. We believe that all of the differences are either formatting differences or copy-editing changes. If you cite these papers, please cite the published version rather than giving a URL.

[Back to the top]

See also Citeseer, Google Scholar, and DB&LP;.

Books

• Reps, T. and Teitelbaum, T., The Synthesizer Generator: A System for Constructing Language-Based Editors. Springer-Verlag, New York, NY, 1988. [abstract]

• Reps, T. and Teitelbaum, T., The Synthesizer Generator Reference Manual: Third Edition. Springer-Verlag, New York, NY, 1988.

  Chinese reprint published by the World Publishing Corporation, Beijing, China, 1991.

• Reps, T., Generating Language-Based Environments. The M.I.T. Press, Cambridge, MA, 1984. (Awarded the 1983 ACM Doctoral Dissertation Award.) [abstract]

[Back to the top]

Journal Publications

• Yorsh, G., Reps, T., Sagiv, M., and Wilhelm, R., Logical characterizations of heap abstractions. To appear in ACM Transactions on Computational Logic (TOCL).

• Reps, T., Schwoon, S., Jha, S., and Melski, D., Weighted pushdown systems and their application to interprocedural dataflow analysis. Science of Computer Programming, to appear. [abstract; PostScript; PDF.]

• Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., and Yannakakis, M., Analysis of recursive state machines. ACM Trans. on Program. Lang. and Syst., to appear.

• Jha, S. and Reps, T., Model checking SPKI/SDSI. In Journal of Computer Security 12, 3-4 (2004), 317-353. [abstract; PDF]

• Anderson, P., Reps, T., and Teitelbaum, T., Design and implementation of a fine-grained software inspection tool. In IEEE Trans. on Software Engineering 29, 8 (Aug. 2003), 721-733.

• Reps, T.W. and Rall, L.B., Computational divided differencing and divided-difference arithmetics. In Higher-Order and Symbolic Computation 16, 1-2 (2003), 93-149. [abstract; tech. report version: PostScript, PDF; talk: Powerpoint]

• Clarke, E.M., Fujita, M., Rajan, P.S., Reps, T., Shankar, S., and Teitelbaum, T., Program slicing for VHDL. In Software Tools for Technology Transfer 4, 1 (Oct. 2002), 125-137. [abstract; paper]

• Sagiv, M., Reps, T., and Wilhelm, R., Parametric shape analysis via 3-valued logic. In ACM Transactions on Programming Languages and Systems 24, 3 (2002), 217-298. [abstract; PostScript; PDF; talk: Powerpoint]

• Reps, T., Undecidability of context-sensitive data-dependence analysis. In ACM Transactions on Programming Languages and Systems 22, 1 (Jan. 2000), pp. 162-186. [abstract; PostScript; PDF]

• Melski, D. and Reps, T., Interconvertibility of a class of set constraints and context-free language reachability. In Theoretical Computer Science 248, 1-2 (Nov. 2000), pp. 29-98. [abstract; PostScript; PDF]

• Siff, M. and Reps, T., Identifying modules via concept analysis. In IEEE Transactions on Software Engineering 25, 6 (Nov./Dec. 1999), pp. 749-768. [abstract; send mail to reps [at] cs [dot] wisc [dot] edu to request a copy of the paper.]

• Reps, T., Program analysis via graph reachability. Information and Software Technology 40, 11-12 (November/December 1998), pp. 701-726. [abstract; tech. report version of the paper: PostScript; PDF; talk: Powerpoint]

• Reps, T., ``Maximal-munch'' tokenization in linear time. ACM Transactions on Programming Languages and Systems 20, 2 (March 1998), pp. 259-273. [abstract; PostScript; PDF]

• Sagiv, M., Reps, T., and Wilhelm, R., Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems 20, 1 (January 1998), pp. 1-50. [abstract; PostScript; PDF]

• Sagiv, M., Reps, T., and Horwitz, S., Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science 167 (1996), 131-170. [abstract; paper]

• Reps, T., On the sequential nature of interprocedural program-analysis problems. Acta Informatica 33 (1996), 739-757. [abstract; paper]

• Ramalingam, G. and Reps, T., An incremental algorithm for a generalization of the shortest-path problem. Journal of Algorithms 21, (1996), 267-305. [abstract; paper]

• Ramalingam, G. and Reps, T., On the computational complexity of dynamic graph problems. Theoretical Computer Science A 158 (May 1996), 233-277. [abstract; paper]

• Binkley, D., Horwitz, S., and Reps, T., Program integration for languages with procedure calls. ACM Transactions on Software Engineering and Methodology 4, 1 (January 1995), pp. 3-35. [abstract; paper]

• Ramalingam, G. and Reps, T., On competitive on-line algorithms for the dynamic priority-ordering problem. Information Processing Letters 51 (1994), 155-161. [abstract; paper]

• Yang, W., Horwitz, S., and Reps, T., A program integration algorithm that accommodates semantics-preserving transformations. ACM Transactions on Software Engineering and Methodology 1, 3 (July 1992), 310-354. [abstract]

• Reps, T., Algebraic properties of program integration. Science of Computer Programming 17 (1991), 139-215. [abstract; paper]

• Horwitz, S. and Reps, T., Efficient comparison of program slices. Acta Informatica 28 (1991), 713-732. [abstract]

• Horwitz, S., Reps, T., and Binkley, D., Interprocedural slicing using dependence graphs. ACM Transactions on Programming Languages and Systems 12, 1 (January 1990), 26-60. [abstract; paper]

• Horwitz, S., Prins, J., and Reps, T., Integrating non-interfering versions of programs. ACM Transactions on Programming Languages and Systems 11, 3 (July 1989), 345-387. [abstract; paper]

• Reps, T. Incremental evaluation for attribute grammars with unrestricted movement between tree modifications. Acta Informatica 25 (1988), 155-178. [abstract]

• Reps, T. and Demers, A., Sublinear-space evaluation algorithms for attribute grammars. ACM Transactions on Programming Languages and Systems 9, 3 (July 1987), 408-440. [abstract; paper, via ACM Digital Library]

• Reps, T., Teitelbaum, T., and Demers, A., Incremental context-dependent analysis for language-based editors. ACM Transactions on Programming Languages and Systems 5, 3 (July 1983), 449-477. [abstract; paper, via ACM Digital Library]

• Teitelbaum, T. and Reps, T., The Cornell Program Synthesizer: A syntax-directed programming environment. Communications of the ACM 24, 9 (September 1981), 563-573. [abstract; paper, via ACM Digital Library]

[Back to the top]

Invited Papers

• Reps, T., Sagiv, M., and Wilhelm, R., Static program analysis via 3-valued logic. In Proc. Int. Conf. on Computer-Aided Verification, 2004, 15-30. [abstract; PostScript; PDF; (c) Springer-Verlag; talk: Powerpoint.]

• Rall, L.B. and Reps, T.W., Algorithmic differencing. In Perspectives on Enclosure Methods, U. Kulisch, R. Lohner, and A. Faciush (eds.), Springer-Verlag, Vienna, 2001, 133-147. (Invited paper presented at SCAN 2000: 9th GAMM-IMACS Int. Symp. on Sci. Comput., Comp. Arith., and Validated Numerics, (Karlsruhe, Ger., Sept. 19-22, 2000).) [abstract]

• Wilhelm, R., Sagiv, M., and Reps, T., Shape analysis. In Proc. of CC 2000: 9th Int. Conf. on Compiler Construction, (Berlin, Ger., Mar. 27 - Apr. 2, 2000). [abstract; PostScript; PDF; (c) Springer-Verlag]

• Reps, T., Program analysis via graph reachability. In Proc. of ILPS '97: International Logic Programming Symposium, (Port Jefferson, NY, Oct. 12-16, 1997), J. Maluszynski (ed.), The M.I.T. Press, Cambridge, MA, 1997, pp. 5-19. [abstract; paper, (c) Springer-Verlag]

• Reps, T., The use of program profiling in software testing. In Proc. of Informatik '97 (Aachen, Germany, Sept. 24-27, 1997), M. Jarke, K. Pasedach, and K. Pohl (eds.), Springer-Verlag, Berlin, Ger., 1997, pp. 4-16. [abstract; paper, (c) Springer-Verlag]

• Horwitz, S. and Reps, T., The use of program dependence graphs in software engineering. In Proceedings of the Fourteenth International Conference on Software Engineering, (May 11-15, 1992, Melbourne, Australia), ACM, New York, NY, 1992, pp. 392-411. [abstract; paper]

• Reps, T. and Horwitz, S., Semantics-based program integration. In Proceedings of the Second European Symposium on Programming, (Nancy, France, March 21-25, 1988), Lecture Notes in Computer Science, Vol. 300, H. Ganzinger (ed.), Springer-Verlag, New York, NY, 1988, pp. 1-20.

[Back to the top]

Book Chapters

• Sagiv, M., Reps, T.W., Wilhelm, R., and Yahav, E., On the utility of canonical abstraction. In Engineering Theories of Software Intensive Systems, M. Broy, J. Gruenbauer, T. Hoare, and D. Harel (eds.), Kluwer Academic Publishers, Dordrecht, The Netherlands, 2005, 215-256.

• Reps, T., Sagiv, M., and Wilhelm, R., Shape analysis and applications. In The Compiler Design Handbook: Optimizations and Machine Code Generation, CRC Press, 2002, 175-217.

• Reps, T., Demand interprocedural program analysis using logic databases. In Applications of Logic Databases, R. Ramakrishnan (ed.), Kluwer Academic Publishers, Boston, MA, 1994, pp. 163-196. [abstract; paper]

[Back to the top]

Reprinted in Collections

• Horwitz, S., Reps, T., and Binkley, D., Interprocedural slicing using dependence graphs. 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation (1979 - 1999): A Selection, K.S. McKinley, ed., ACM SIGPLAN Notices 39, 4 (April 2004), 232-243. [abstract]

  Reprinted from Proceedings of the ACM SIGPLAN 88 Conference on Programming Language Design and Implementation, (Atlanta, GA, June 22-24, 1988), ACM SIGPLAN Notices 23, 7 (July 1988), pp. 35-46.

  A retrospective on the paper was published as

  Horwitz, S., Reps, T., and Binkley, D., Retrospective: Interprocedural slicing using dependence graphs. 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation (1979 - 1999): A Selection, K.S. McKinley, ed., ACM SIGPLAN Notices 39, 4 (April 2004), 229-231. [retrospective (PS); retrospective (PDF)]

• Horwitz, S., Reps, T., and Binkley, D., Interprocedural slicing using dependence graphs. In Software Change Impact Analysis, S.A. Bohner and R.S. Arnold (eds.), IEEE Computer Society, Los Alamitos, CA, 1996.

  Reprinted from ACM Transactions on Programming Languages and Systems 12, 1 (January 1990), 26-60. [abstract; paper]

• Horwitz, S., Reps, T., and Binkley, D., Interprocedural slicing using dependence graphs. In Software Merging and Slicing, V. Berzins (ed.), IEEE Computer Society, Los Alamitos, CA, pp. 10-44.

  Reprinted from ACM Transactions on Programming Languages and Systems 12, 1 (January 1990), 26-60. [abstract; paper]

• Horwitz, S., Prins, J., and Reps, T., Integrating non-interfering versions of programs. In Software Merging and Slicing, V. Berzins (ed.), IEEE Computer Society, Los Alamitos, CA, pp. 137-179.

  Reprinted from ACM Transactions on Programming Languages and Systems 11, 3 (July 1989), 345-387. [abstract; paper]

• Ramalingam, G. and Reps, T., A theory of program modifications. In Software Merging and Slicing, V. Berzins (ed.), IEEE Computer Society, Los Alamitos, CA, 90-105.

  Reprinted from Proceedings of the Colloquium on Combining Paradigms for Software Development, (Brighton, UK, April 8-12, 1991), Lecture Notes in Computer Science, Vol. 494, S. Abramsky and T.S.E. Maibaum (eds.), Springer-Verlag, New York, NY, 1991, pp. 137-152.

• Reps, T. and Teitelbaum, T., Language processing in program editors. In Language Architectures and Programming Environments, T. Ichikawa and H. Tsubotani (eds.), The World Scientific Publishing Company, Singapore, 1992, pp. 146-169.

  Reprinted from IEEE Computer 20, 11 (November 1987), 29-40.

• Teitelbaum, T. and Reps, T., The Cornell Program Synthesizer: A syntax-directed programming environment. In Interactive Programming Environments, D. Barstow, E. Sandewall, and H. Shrobe (eds.), McGraw-Hill, 1984, pp. 97-116.

  Reprinted from Communications of the ACM 24, 9 (September 1981), 563-573. [abstract; paper, via ACM Digital Library]

• Teitelbaum, T., Reps, T., and Horwitz, S., The why and wherefore of the Cornell Program Synthesizer. In Software Development Environments, A.I. Wasserman (ed.), IEEE Computer Society, Washington, DC, 1981, 64-72.

  Reprinted from Proceedings of the ACM SIGPLAN/SIGOA Symposium on Text Manipulation, (Portland, OR, June 8-10, 1981), ACM SIGPLAN Notices 16, 6 (June 1981), pp. 8-16.

[Back to the top]

Magazine Articles

• Anderson, P., Reps, T., Teitelbaum, T., and Zarins, M., Tool support for fine-grained software inspection. IEEE Software 20(4): 42-50 (2003).

• Reps, T. and Teitelbaum, T., Language processing in program editors. IEEE Computer 20, 11 (November 1987), 29-40.

[Back to the top]

Conference Publications

• Jeannet, B., Gopan, B., and Reps, T., A relational abstraction for functions. To appear in Proc. 12th Int. Static Analysis Symp., 2005.

• Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S., and Yorsh, G., Simulating reachability using first-order logic with applications to verification of linked data structures. To appear in Proc. Conf. on Automated Deduction, 2005. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Balakrishnan, G., Reps, T., Kidd, N., Lal, A., Lim, J., Melski, D., Gruian, R., Yong, S., Chen, C.-H., and Teitelbaum, T., Model checking x86 executables with CodeSurfer/x86 and WPDS++, (tool-demonstration paper). In Proc. Computer-Aided Verification, 2005. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Lal, A., Balakrishnan, G., and Reps, T., Extended weighted pushdown systems. To appear in Proc. Computer-Aided Verification, 2005. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Loginov, A., Reps, T, and Sagiv, M., Abstraction refinement via inductive learning. To appear in Proc. Computer-Aided Verification, 2005. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Ganapathy, V., Seshia, S.A., Jha, S., Reps, T.W., and Bryant, R.E., Automatic discovery of API-level exploits. To appear in Proc. Int. Conf. on Software Engineering, (St. Louis, Missouri, May 15-21, 2005). [abstract; PostScript; PDF]

• Balakrishnan, G., Gruian, R., Reps, T., and Teitelbaum, T., CodeSurfer/x86 -- A platform for analyzing x86 executables, (tool demonstration paper). To appear in Proc. Int. Conf. on Compiler Construction, April 2005. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Jeannet, B., Gopan, D., and Reps, T., A relational abstraction for functions. In Int. Workshop on Numerical and Symbolic Abstract Domains, Jan. 2005. [abstract; PostScript; PDF]

• Yorsh, G., Skidanov, A., Reps, T., and Sagiv, M., Assume/guarantee reasoning for heap-manipulating programs. In 1st Int. Workshop on Abstract Interpretation of Object-Oriented Languages, Jan. 2005. [abstract; PostScript; PDF]

• Gopan, D., Reps, T., and Sagiv, M., Numeric analysis of array operations. In Conference Record of the Thirty-Second ACM Symposium on Principles of Programming Languages, (Long Beach, CA, Jan. 12-14, 2005), 338-350. [abstract; PostScript; PDF]

• Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., and Wilhelm, R., A semantics for procedure local heaps and its abstractions. In Conference Record of the Thirty-Second ACM Symposium on Principles of Programming Languages, (Long Beach, CA, Jan. 12-14, 2005), 296-309. [abstract; PDF]

• Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G., The boundary between decidability and undecidability for transitive closure logics. In Proc. Computer Science Logic, Lecture Notes in Computer Science, Springer-Verlag, New York, NY, 2004. [abstract]

• Jeannet, B., Loginov, A., Reps, T., and Sagiv, M., A relational approach to interprocedural shape analysis. In Proc. 11th Int. Static Analysis Symp., Lecture Notes in Computer Science, Springer-Verlag, New York, NY, 2004. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G., Verification via structure simulation. In Proc. Int. Conf. on Computer-Aided Verification, 2004, 281-294. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Balakrishnan, G. and Reps, T. Analyzing memory accesses in x86 executables. In Proc. Int. Conf. on Compiler Construction, Springer-Verlag, New York, NY, 2004, 5-23. (Awarded the EAPLS Best Paper Award at ETAPS 2004.) [abstract; PostScript; PDF; (c) Springer-Verlag; talk: Powerpoint]

• Yorsh, G., Reps, T., and Sagiv, M., Symbolically computing most-precise abstract operations for shape analysis. In Proc. TACAS, Springer-Verlag, New York, NY, 2004, 530-545. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Gopan, D., DiMaio, F., Dor, N., Reps, T., and Sagiv, M., Numeric domains with summarized dimensions. In Proc. TACAS, Springer-Verlag, New York, NY, 2004, 512-529. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Reps, T., Sagiv, M., and Yorsh, G., Symbolic implementation of the best transformer. In Proc. Verification, Model Checking, and Abstract Interpretation, 2004, 252-266. [abstract; PostScript; PDF; (c) Springer-Verlag]

• T. Reps, S. Schwoon, and S. Jha, Weighted pushdown systems and their application to interprocedural dataflow analysis. In Proc. 10th Int. Static Analysis Symp., (June 11-13, 2003, San Diego, CA), Lecture Notes in Computer Science, Vol. 2694, Springer-Verlag, New York, NY, 2003, pp. 189-213. [abstract; PostScript; PDF; (c) Springer-Verlag; talk: Powerpoint]

• S. Schwoon, S. Jha, T. Reps, and S. Stubblebine, On generalized authorization problems. In Proc. 16th IEEE Computer Security Foundations Workshop, (June 30 - July 2, 2003, Asilomar, Pacific Grove, CA), pp. 202-218. [abstract; PostScript, PDF; talk: Powerpoint.]

• Reps, T., Sagiv, M., and Loginov, A., Finite differencing of logical formulas for static analysis. In Proc. European Symp. on Programming, Lecture Notes in Computer Science, Vol. 2618, Springer-Verlag, New York, NY, 2003, pp. 380-398. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Yahav, E., Reps, T., Sagiv, M., and Wilhelm, R. Verifying temporal heap properties specified via evolution logic. In Proc. European Symp. on Programming, Lecture Notes in Computer Science, Vol. 2618, Springer-Verlag, New York, NY, 2003, pp. 204-222. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Melski, D and Reps, T., The interprocedural express-lane transformation. In Proc. Int. Conf. on Compiler Construction, Lecture Notes in Computer Science, Vol. 2622, Springer-Verlag, New York, NY, 2003, pp. 200-216. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Reps, T., Loginov, A., and Sagiv, M., Semantic minimization of 3-valued propositional formulae. In Proc. IEEE Symp. on Logic in Computer Science, (Copenhagen, Denmark, July 22-25, 2002), pp. 40-54. [abstract; PostScript; PDF]

• Jha, S. and Reps, T., Analysis of SPKI/SDSI certificates using model checking. In Proc. 15th IEEE Computer Security Foundations Workshop, (Cape Breton, Nova Scotia, June 24-26, 2002), pp. 129-146. [abstract; PostScript; PDF]

• Benedikt, M., Godefroid, P., and Reps, T., Model checking of unrestricted hierarchical state machines. In Proc. of ICALP 2001, Twenty-Eighth Int. Colloq. on Automata, Languages, and Programming, (Crete, Greece, July 8-12, 2001), Lecture Notes in Computer Science, Vol. 2076, Springer-Verlag, New York, NY, 2001, pp. 652-666. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Loginov, A., Yong, S.H., Horwitz, S., and Reps, T., Debugging via run-time type checking. In Proc. of FASE 2001: Fundamental Approaches to Softw. Eng., (Genoa, Italy, April 2-6, 2001). [abstract; PostScript; PDF; (c) Springer-Verlag]

• Xu, Z., Reps, T., and Miller, B., Typestate checking of machine code. In Proc. of ESOP 2001: European Symp. on Programming, (Genoa, Italy, April 2-6, 2001). [abstract; PostScript; PDF; (c) Springer-Verlag]

• Lev-Ami, T., Reps, T., Sagiv, M., and Wilhelm, R., Putting static analysis to work for verification: A case study. In ISSTA 2000: Proc. of the Int. Symp. on Software Testing and Analysis, (Portland, OR, Aug. 21-25, 2000). [abstract; PostScript; PDF]

• Xu, Z., Miller, B., and Reps, T., Safety checking of machine code. In SIGPLAN '00: Proceedings of the ACM Conference on Programming Language Design and Implementation, (Vancouver B.C., Canada, June 18-21, 2000), pp. 70-82. [abstract; paper]

• Chandra, S. and Reps, T., Physical type checking for C. In Proc. of PASTE '99: SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, (Toulouse, France, Sept. 6, 1999). ACM SIGSOFT Software Engineering Notes 24, 5 (Sept. 1999), pp. 66-75. [abstract; PostScript; PDF]

• Siff, M., Chandra, S., Ball, T., Kunchithapadam, K., and Reps, T., Coping with type casts in C. In Proceedings of ESEC/FSE '99: Seventh European Software Engineering Conference and Seventh ACM SIGSOFT Symposium on the Foundations of Software Engineering, (Toulouse, France, Sept. 6-10, 1999), pp. 180-198. [abstract; PostScript; PDF]

• Clarke, E.M., Fujita, M., Rajan, P.S., Reps, T., Shankar, S., and Teitelbaum, T., Program slicing of hardware description languages. In Proc. of Charme '99, (Bad Herrenalb, Ger., Sept. 27-29, 1999). [abstract; PostScript; PDF]

• Yong, S.H., Horwitz, S., and Reps, T., Pointer analysis for programs with structures and casting. In SIGPLAN '99: Proceedings of the ACM Conference on Programming Language Design and Implementation, (Atlanta, GA, May 1-4, 1999), ACM SIGPLAN Notices 34, 5 (May 1999), pp. 91-103. [abstract; PostScript; PDF]

• Melski, D. and Reps, T., Interprocedural path profiling. In Proc. of CC '99: 8th Int. Conf. on Compiler Construction, (Amsterdam, The Netherlands, Mar. 22-26, 1999), Lecture Notes in Computer Science, Vol. 1575, S. Jaehnichen (ed.), Springer-Verlag, New York, NY, 1999, pp. 47-62. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Benedikt, M., Reps, T., and Sagiv, M., A decidable logic for describing linked data structures. In Proc. of ESOP '99: European Symposium on Programming, (Amsterdam, The Netherlands, Mar. 22-26, 1999), Lecture Notes in Computer Science, Vol. 1576, S.D. Swierstra (ed.), Springer-Verlag, New York, NY, 1999, pp. 2-19. [abstract; PostScript; PDF; (c) Springer-Verlag]

• Sagiv, M., Reps, T., and Wilhelm, R., Parametric shape analysis via 3-valued logic. In Conference Record of the Twenty-Sixth ACM Symposium on Principles of Programming Languages, (San Antonio, TX, Jan. 20-22, 1999), ACM, New York, NY, 1999, pp. 105-118. [abstract; PostScript; PDF]

• Siff, M. and Reps, T., Identifying modules via concept analysis. In ICSM '97: IEEE International Conference on Software Maintenance, (Oct. 1-3, 1997, Bari, Italy), M.J. Harrold and G. Visaggio (eds.), IEEE Computer Society, Washington, DC, 1997, pp. 170-179. [abstract; PostScript; PDF]

• Reps, T., Ball, T., Das, M., and Larus, J., The use of program profiling for software maintenance with applications to the Year 2000 Problem. In Proceedings of ESEC/FSE '97: Sixth European Software Engineering Conference and Fifth ACM SIGSOFT Symposium on the Foundations of Software Engineering, (Zurich, Switzerland, Sept. 22-25, 1997), Lecture Notes in Computer Science, Vol. 1301, M. Jazayeri and H. Schauer (eds.), Springer-Verlag, New York, NY, 1997, pp. 432-449. [abstract; paper, (c) Springer-Verlag]

• Melski, D. and Reps, T., Interconvertibility of set constraints and context-free language reachability. In PEPM '97: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, (Amsterdam, The Netherlands, June 12-13, 1997), ACM, New York, NY, 1997, pp. 74-89. [abstract; paper]

• Siff, M. and Reps, T., Program generalization for software reuse: From C to C++. In SIGSOFT 96: Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, (San Francisco, CA, October 16-18, 1996), ACM, New York, NY, 1996, pp. 135-146. [abstract; paper]

• Reps, T. and Turnidge, T., Program specialization via program slicing. In Proceedings of the Dagstuhl Seminar on Partial Evaluation, (Schloss Dagstuhl, Wadern, Germany, Feb. 12-16, 1996), Lecture Notes in Computer Science, Vol. 1110, O. Danvy, R. Glueck, and P. Thiemann (eds.), Springer-Verlag, New York, NY, 1996, pp. 409-429. [abstract; paper, (c) Springer-Verlag]

• Sagiv, M., Reps, T., and Wilhelm, R., Solving shape-analysis problems in languages with destructive updating. In Conference Record of the Twenty-Third ACM Symposium on Principles of Programming Languages, (St. Petersburg, FL, Jan. 22-24, 1996), ACM, New York, NY, 1996, pp. 16-31. [abstract; paper]

• Horwitz, S., Reps, T., and Sagiv, M., Demand interprocedural dataflow analysis. In SIGSOFT '95: Proceedings of the Third ACM SIGSOFT Symposium on the Foundations of Software Engineering, (Washington, DC, October 10-13, 1995), ACM SIGSOFT Software Engineering Notes 20, 4 (1995), pp. 104-115. [abstract; paper]

• Reps, T. and Rosay, G., Precise interprocedural chopping. In SIGSOFT '95: Proceedings of the Third ACM SIGSOFT Symposium on the Foundations of Software Engineering, (Washington, DC, October 10-13, 1995), ACM SIGSOFT Software Engineering Notes 20, 4 (1995), pp. 41-52. [abstract; paper]

• Das, M., Reps, T., and Van Hentenryck, P. Semantic foundations of binding-time analysis for imperative programs. In PEPM '95: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, (La Jolla, California, June 21-23, 1995), ACM, New York, NY, 1995, pp. 100-110. [abstract; paper]

• Reps, T., Shape analysis as a generalized path problem. In PEPM '95: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, (La Jolla, California, June 21-23, 1995), ACM, New York, NY, 1995, pp. 1-11. [abstract; PostScript; PDF]

• Sagiv, M., Reps, T., and Horwitz, S., Precise interprocedural dataflow analysis with applications to constant propagation. In Proceedings of FASE '95: Colloquium on Formal Approaches in Software Engineering, (Aarhus, Denmark, May 22-26, 1995), Lecture Notes in Computer Science, Vol. 915, P.D. Mosses, M. Nielsen, and M.I. Schwartzbach (eds.), Springer-Verlag, New York, NY, 1995, pp. 651-665. [abstract; paper, (c) Springer-Verlag]

• Reps, T., Horwitz, S., and Sagiv, M., Precise interprocedural dataflow analysis via graph reachability. In Conference Record of the Twenty-Second ACM Symposium on Principles of Programming Languages, (San Francisco, CA, Jan. 23-25, 1995), pp. 49-61. [abstract; PostScript; PDF]

• Reps, T., Horwitz, S., Sagiv, M., and Rosay, G., Speeding up slicing. In SIGSOFT '94: Proceedings of the Second ACM SIGSOFT Symposium on the Foundations of Software Engineering, (New Orleans, LA, December 7-9, 1994), ACM SIGSOFT Software Engineering Notes 19, 5 (December 1994), pp. 11-20. [abstract; PostScript; PDF]

• Reps, T., Solving demand versions of interprocedural analysis problems. In Proceedings of the Fifth International Conference on Compiler Construction, (Edinburgh, Scotland, April 7-9, 1994), Lecture Notes in Computer Science, Vol. 786, P. Fritzson (ed.), Springer-Verlag, New York, NY, 1994, pp. 389-403. [abstract; paper, (c) Springer-Verlag]

• Ramalingam, G. and Reps, T., An incremental algorithm for maintaining the dominator tree of a reducible flowgraph. In Conference Record of the Twenty-First ACM Symposium on Principles of Programming Languages, (Portland, OR, Jan. 16-19, 1994), pp. 287-296. [abstract; PostScript; PDF]

• Reps, T., Scan grammars: Parallel attribute evaluation via data-parallelism. In Proceedings of the Fifth ACM Symposium on Parallel Algorithms and Architectures, (Velen, Germany, June 30 - July 2, 1993). [abstract; PostScript; PDF]

• Ramalingam, G. and Reps, T., Modification algebras. In Proceedings of the Second International Conference on Algebraic Methodology and Software Technology (AMAST), (Iowa City, Iowa, May 22-24, 1991).

• Ramalingam, G. and Reps, T., A theory of program modifications. In Proceedings of the Colloquium on Combining Paradigms for Software Development, (Brighton, UK, April 8-12, 1991), Lecture Notes in Computer Science, Vol. 494, S. Abramsky and T.S.E. Maibaum (eds.), Springer-Verlag, New York, NY, 1991, pp. 137-152.

• Yang, W., Horwitz, S., and Reps, T., A program integration algorithm that accommodates semantics-preserving transformations. In SIGSOFT '90: Proceedings of the Fourth ACM SIGSOFT Symposium on Software Development Environments, (Irvine, CA, December 3-5, 1990), ACM Software Engineering Notes 15, 6 (December 1990), pp. 133-143.

• Reps, T., Algebraic properties of program integration. In Proceedings of the 3nd European Symposium on Programming (Copenhagen, Denmark, May 15-18, 1990), Lecture Notes in Computer Science, Vol. 432, N. Jones (ed.), Springer-Verlag, New York, NY, 1990, pp. 326-340.

• Reps, T. and Bricker, T., Illustrating interference in interfering versions of programs. In Proceedings of the Second International Workshop on Software Configuration Management, (Princeton, NJ, October 24-27, 1989), ACM Software Engineering Notes 17, 7 (November 1989), pp. 46-55.

• Horwitz, S., Pfeiffer, P., and Reps, T., Dependence analysis for pointer variables. In Proceedings of the ACM SIGPLAN 89 Conference on Programming Language Design and Implementation, (Portland, OR, June 21-23, 1989), ACM SIGPLAN Notices 24, 7 (July 1989), pp. 28-40.

• Reps, T. and Yang, W., The semantics of program slicing and program integration. In Proceedings of the Colloquium on Current Issues in Programming Languages, (Barcelona, Spain, March 13-17, 1989), Lecture Notes in Computer Science, Vol. 352, J. Diaz and F. Orejas (eds.), Springer-Verlag, New York, NY, 1989, pp. 360-374.

• Horwitz, S., Reps, T., and Binkley, D., Interprocedural slicing using dependence graphs. In Proceedings of the ACM SIGPLAN 88 Conference on Programming Language Design and Implementation, (Atlanta, GA, June 22-24, 1988), ACM SIGPLAN Notices 23, 7 (July 1988), pp. 35-46. [abstract; retrospective (PS); retrospective (PDF)]

• Reps, T., Horwitz, S., and Prins, J., Support for integrating program variants in an environment for programming in the large. In Proceedings of the International Workshop on Software Version and Configuration Control, (Grassau, W. Germany, Jan. 27-29, 1988), Berichte des German Chapter of the ACM, Vol. 30, J.F.H. Winkler (ed.), B.G. Teubner, Stuttgart, W. Germany, 1988, pp. 197-216.

• Horwitz, S., Prins, J., and Reps, T., Integrating non-interfering versions of programs. In Conference Record of the Fifteenth ACM Symposium on Principles of Programming Languages, (San Diego, CA, January 13-15, 1988), ACM, New York, NY, 1988, pp. 133-145.

• Horwitz, S., Prins, J., and Reps, T., On the adequacy of program dependence graphs for representing programs. In Conference Record of the Fifteenth ACM Symposium on Principles of Programming Languages, (San Diego, CA, January 13-15, 1988), ACM, New York, NY, 1988, pp. 146-157. [abstract; paper]

• Reps, T., Marceau, C., and Teitelbaum, T., Remote attribute updating for language-based editors. In Conference Record of the Thirteenth ACM Symposium on Principles of Programming Languages, (St. Petersburg, FL, January 13-15, 1986), ACM, New York, NY, 1986, pp. 1-13.

• Reps, T. and Teitelbaum, T., The Synthesizer Generator. In Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, (Pittsburgh, PA, April 23-25, 1984), ACM SIGPLAN Notices 19, 5 (May 1984), pp. 42-48. [abstract]

• Reps, T. and Alpern, B., Interactive proof checking. In Conference Record of the Eleventh ACM Symposium on Principles of Programming Languages, (Salt Lake City, Utah, January 15-18, 1984), ACM, New York, NY, 1984, pp. 36-45. [abstract]

• Reps, T., Static-semantic analysis in language-based editors. In Digest of Papers of the IEEE Spring CompCon 83, (San Francisco, CA, March 1-3, 1983), IEEE Computer Society, Washington, DC, 1983, pp. 411-414.

• Reps, T., Optimal-time incremental semantic analysis for syntax-directed editors. In Conference Record of the Ninth ACM Symposium on Principles of Programming Languages, (Albuquerque, NM, January 25-27, 1982), ACM, New York, NY, 1982, pp. 169-176. [abstract]

• Teitelbaum, T., Reps, T., and Horwitz, S., The why and wherefore of the Cornell Program Synthesizer. In Proceedings of the ACM SIGPLAN/SIGOA Symposium on Text Manipulation, (Portland, OR, June 8-10, 1981), ACM SIGPLAN Notices 16, 6 (June 1981), pp. 8-16.

• Demers, A., Reps, T., and Teitelbaum, T., Incremental evaluation for attribute grammars with application to syntax-directed editors. In Conference Record of the Eighth ACM Symposium on Principles of Programming Languages, (Williamsburg, VA, January 26-28, 1981), ACM, New York, NY, 1981, pp. 105-116. [abstract]

[Back to the top]

Software

• Reps, T., Rosay, G., and Horwitz, S., The Wisconsin Program-Slicing Tool. Release 1.0, August 1997. (Click here for license information.)

• Reps, T., Bricker, T., Rosay, G., et al., The Wisconsin Program-Integration System. Release 0.5, April 1990; Release 1.0, April 1992. Release 2.0, July 1993. Licensed to 9 sites.

• Reps, T., Teitelbaum, T., et al., The Synthesizer Generator. Release 1.0, December 1985; Release 2.0, July 1987; Release 3.0, April 1989. Licensed to approximately 325 sites.

• Teitelbaum, T., Reps, T., et al., The Cornell Program Synthesizer. Version 1, June 1979; Version 1.02, September 1980; Version 1.03, September 1981. Licensed to approximately 110 sites.

[Back to the top]

Patents

• Reps, T., Horwitz, S., and Binkley, D., Interprocedural slicing of computer programs using dependence graphs. U.S. Patent Number 5,161,216, issued November 3, 1992.

[Back to the top]

Pending Submissions

[Back to the top]

Other Publications and Reports

• Loginov, A., Reps, T, and Sagiv, M., Learning abstractions for verifying data-structure properties. TR-1519, Computer Sciences Department, University of Wisconsin, Madison, WI, Jan. 2005. [abstract; PostScript; PDF]

• Ganapathy, V., Seshia, S.A., Jha, S., Reps, T.W., and Bryant, R.E., Automatic discovery of API-level vulnerabilities. TR-1512, Computer Sciences Department, University of Wisconsin, Madison, WI, July 2004. PDF]

• Loginov, A., Reps, T, and Sagiv, M., Abstraction refinement for 3-valued-logic analysis. TR-1504, Computer Sciences Department, University of Wisconsin, Madison, WI, April 2004. [abstract; PostScript; PDF]

• Yahav, E., Pnueli, A., Reps, T., and Sagiv, M., Automatic verification of temporal heap properties. April 2004.

• Bauer, J., Rinetzky, N., Reps, T., Sagiv, M., and Wilhelm, R., Semantic requirements for modular reasoning about heap-manipulating programs. Oct. 2003.

• Yahav, E., Reps, T., and Sagiv, M., LTL model checking for systems with unbounded number of dynamically created threads and objects. TR-1424, Computer Sciences Department, University of Wisconsin, Madison, WI, March 2001. [abstract; PostScript; PDF]

• Chandra, S. and Reps, T., Physical type checking for C. Bell Labs. Tech. Rep. BL0113590-990302-04, Lucent Technologies, Inc., Naperville, IL, Mar. 1999. [abstract; PostScript; PDF]

• Siff, M., Chandra, S., Ball, T., Kunchithapadam, K., and Reps, T., Coping with type casts in C. Bell Labs. Tech. Rep. BL0113590-990202-03, Lucent Technologies, Inc., Naperville, IL, Feb. 1999. [abstract; PostScript; PDF]

• Clarke, E.M., Fujita, M., Rajan, P.S., Reps, T., Shankar, S., and Teitelbaum, T., Program slicing for design automation: An automatic technique for speeding-up hardware design, simulation, testing, and verification. Unpublished report, October 1998. [abstract; paper]

• Melski, D. and Reps, T., Interprocedural path profiling. TR-1382, Computer Sciences Department, University of Wisconsin, Madison, WI, September 1998. [abstract; PostScript; PDF]

• Reps, T., Program analysis via graph reachability. TR-1386, Computer Sciences Department, University of Wisconsin, Madison, WI, August 1998. [abstract; PostScript; PDF; talk: Powerpoint]

• Mueller, H., Reps, T., and Snelting, G. (eds.), Program comprehension and software reengineering. Dagstuhl Seminar Report, International Conference and Research Center for Computer Science (IBFI), Schloss Dagstuhl, Wadern, Germany, 1998. dag9810.ps

• The Wisconsin Program-Slicing Tool 1.0, Reference Manual. Computer Sciences Department, University of Wisconsin-Madison, August 1997. slicing-manual.ps

• Das, M. and Reps, T. BTA termination using CFL-reachability. TR-1329, Computer Sciences Department, University of Wisconsin, Madison, WI, November 1996.

• Horwitz, S., Reps, T., and Sagiv, M., Demand interprocedural dataflow analysis. TR-1283, Computer Sciences Department, University of Wisconsin, Madison, WI, August 1995. tr1283r.ps

• Reps, T., Sagiv, M., and Wilhelm, R., Solving shape-analysis problems in languages with destructive updating. TR-1276, Computer Sciences Department, University of Wisconsin, Madison, WI, July 1995. tr1276.ps

• van Leeuwen, J., Mehlhorn, K., and Reps, T. (eds.), Incremental computation and dynamic algorithms. Dagstuhl Seminar Report 88, International Conference and Research Center for Computer Science (IBFI), Schloss Dagstuhl, Wadern, Germany, 1994. dagstuhl.sr88.ps

• Reps, T., Sagiv, M., and Horwitz S., Interprocedural dataflow analysis via graph reachability. TR 94-14, Datalogisk Institut, University of Copenhagen, Copenhagen, Denmark, April 1994. diku-tr94-14.ps

• Reps, T., The Wisconsin Program-Integration System Reference Manual: Release 2.0. Computer Sciences Department, University of Wisconsin-Madison, July 1993. manual.2.0.ps

• Ramalingam, G. and Reps, T., A categorized bibliography on incremental computation. In Conference Record of the Twentieth ACM Symposium on Principles of Programming Languages, (Charleston, SC, Jan. 11-13, 1993), ACM, New York, NY, 1993, pp. 502-510. (Tutorial paper.)

• Reps, T., Incremental computation. Unpublished tutorial notes, 1993. (Presented at the Twentieth ACM Symposium on Principles of Programming Languages, (Charleston, SC, Jan. 11-13, 1993).)

• Klint, P., Reps, T., and Snelting, G. (eds.), Programming environments. Dagstuhl Seminar Report 34, International Conference and Research Center for Computer Science (IBFI), Schloss Dagstuhl, Wadern, Germany, 1992.

• Binkley, D., Horwitz, S., and Reps, T., Identifying semantic differences in programs with procedures (Extended abstract). Computer Sciences Department, University of Wisconsin-Madison, September 1991.

• Ramalingam, G. and Reps, T., New programs from old. TR-1057, Computer Sciences Department, University of Wisconsin-Madison, November 1991. [paper; latest version]

• Ball, T., Horwitz, S., and Reps, T., Correctness of an algorithm for reconstituting a program from a dependence graph. TR-947, Computer Sciences Department, University of Wisconsin-Madison, July 1990.

• Ramalingam, G. and Reps, T., Semantics of program representation graphs. TR-900, Computer Sciences Department, University of Wisconsin-Madison, December 1989. [paper]

• Binkley, D., Horwitz, S., and Reps, T., The multi-procedure equivalence theorem. TR-890, Computer Sciences Department, University of Wisconsin-Madison, November 1989. [paper]

• Reps, T. Demonstration of a prototype tool for program integration. TR-819, Computer Sciences Department, University of Wisconsin-Madison, January 1989. [paper]

[Back to the top]

Visitors and Post-Doctoral Associates

• Neil Immerman (U. Mass.), 2004-05.

• Bertrand Jeannet (IRISA), Mar. - June, 2003.

• Stefan Schwoon (Univ. of Stuttgart), Feb. - Mar., 2003.

• David Melski, 2002. (Currently with GrammaTech, Inc., Ithaca, NY.)

• Mooly Sagiv, 1994-95. (Currently Senior Lecturer (tenured), School of Computer Science, Tel-Aviv University, Israel.)

• Robert Paige (NYU), 1990-91.

• Jiazhen Cai (NYU), 1990-91.

• Wuu Yang, 1990-91. (Currently Professor, Department of Computer and Information Science, National Chiao-Tung University, Taiwan.)

• Jan Prins , 1986-87. (Currently Professor, Department of Computer Science, University of North Carolina, Chapel Hill.)

Former Students

• Melski, D. Interprocedural path profiling and the interprocedural express-lane transformation. Ph.D. dissertation and Tech. Rep. TR-1435, Computer Sciences Department, University of Wisconsin, Madison, WI, February 2002. [abstract; PostScript; PDF]

• Xu, Z. Safety-checking of machine code. Ph.D. dissertation, Computer Sciences Department, University of Wisconsin, Madison, WI, December 2000. (Supervised jointly with B. Miller.) [abstract; PostScript; PDF]

• Siff, M., Techniques for software renovation. Ph.D. dissertation and Tech. Rep. TR-1384, Computer Sciences Department, University of Wisconsin, Madison, WI, August 1998. [abstract; dissertation]

• Das, M., Partial evaluation using dependence graphs. Ph.D. dissertation and Tech. Rep. TR-1362, Computer Sciences Department, University of Wisconsin, Madison, WI, February 1998. [abstract; dissertation]

• Ramalingam, G., Bounded incremental computation. Ph.D. dissertation and Tech. Rep. TR-1172, Computer Sciences Department, University of Wisconsin, Madison, WI, August 1993.

  Dissertation published as: Ramalingam, G., Bounded Incremental Computation, Lecture Notes in Computer Science, Vol. 1089, Springer-Verlag, New York, NY, 1996.

• Binkley, D., Multi-procedure program integration. Ph.D. dissertation and Tech. Rep. TR-1038, Computer Sciences Department, University of Wisconsin, Madison, WI, August 1991. [dissertation]

• Pfeiffer, P., Dependence-based representations for programs with reference variables. Ph.D. dissertation and Tech. Rep. TR-1037, Computer Sciences Department, University of Wisconsin, Madison, WI, August 1991. [dissertation (7.2 MB)]

• Yang, W., A new algorithm for semantics-based program integration. Ph.D. dissertation and Tech. Rep. TR-962, Computer Sciences Department, University of Wisconsin, Madison, WI, August 1990. (Supervised jointly with S. Horwitz.) [dissertation]

Current Students

• Gogul Balakrishnan

• Denis Gopan

• Nick Kidd

• Akash Lal

• Junghee Lim

• Alexey Loginov

[Back to the top]