Wisconsin Program-Slicing Project's Home Page (original) (raw)

Disclaimer
Research Summary
Recent Items of Note (Last updated: March. 27, 2025)
Personnel
Categorized Index to Project Publications
Project Bibliography
- Books
- Journal Publications
- Invited Papers
- Book Chapters
- Reprinted in Collections
- Edited Books
- Conference and Refereed Workshop Publications
- Tutorials
- Patents
- Pending Submissions
- Ph.D. Dissertations
- Magazine Articles
- [Other Publications and Reports](#other publications)
Software

Disclaimer

This web page contains links to PostScript and PDF files of articles that may be covered by copyright. You may browse the articles at your convenience (in the same spirit that you read a journal article or an article from a conference proceedings in a public library). Retrieving, copying, or distributing these files may violate copyright law.

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 Table of Contents]

Research Summary

The goal of this project is to create enhanced tools to support the development of complex software systems. The objective is to create tools that provide powerful language-specific program-manipulation operations. In particular, the project has explored how program slicing can serve as the basis for such program-manipulation operations.

The slice of a program with respect to a set of program elements S is a projection of the program that includes only program elements that might affect (either directly or transitively) the values of the variables used at members of S. Slicing allows one to find semantically meaningful decompositions of programs, where the decompositions consist of elements that are not textually contiguous.

Program slicing is a fundamental operation that can aid in solving many software-engineering problems. For instance, it has applications to program understanding, maintenance, debugging, testing, differencing, specialization, reuse, and merging.

The activities of the project have been devoted to:

improving the underlying technology for program slicing (and related operations),
implementing program slicers,
developing methods for using slicing in software-engineering tools, and
building slicing-based program-manipulation tools.

More recently, we found some unexpected connections between interprocedural dataflow analysis and our previous work on interprocedural program slicing. In particular, we have shown how a large class of interprocedural dataflow-analysis problems can be solved by transforming them into a special kind of graph-reachability problem. This graph-reachability problem can be solved precisely in polynomial time by the algorithm originally developed for interprocedural slicing.

[Back to the Table of Contents]

Recent Items of Note

Recent Publications

``Automated abstract transformer synthesis for reduced product domains''
``Verifying solutions to semantics-guided synthesis problems''
``Semantics of sets of programs''
``Scalable equivalence checking and verification of shallow quantum circuits''
``Polynomial bounds of CFLOBDDs against BDDs''
``Synthesizing abstract transformers for reduced-product domains''
``Weighted context-free-language ordered binary decision diagrams''
``Automating pruning in top-down enumeration for program synthesis problems with monotonic semantics''
``Synthesizing formal semantics from executable interpreters''
``Automating unrealizability logic: Hoare-style proof synthesis for infinite sets of programs''
``Newtonian program analysis of probabilistic programs''
``CFLOBDDs: Context-free-language ordered binary decision diagrams''
``Prompt tuning strikes back: Customizing foundation models with low-rank prompt adaptation''
``The SemGuS Toolkit''
``Modular system synthesis''
``Symbolic quantum simulation with Quasimodo''
``Synthesizing specifications''
``Single-source-single-target interleaved-Dyck reachability via integer linear programming''
``Unrealizability logic''

[Back to the Table of Contents]

Miscellaneous

Tips on writing a research paper (video recording from PLMW@PLDI21)
Some notes on automatic differentiation and back-propagation (PDF)
A recording of a lecture about "retrograde debugging" is availablehere. The password is Rptp6tSh. The lecture is based on several "retrograde chess puzzles" from the Raymond Smullyan book "The Chess Mysteries of Sherlock Holmes. Smullyan also wrote a second book of such problems, titled "The Chess Mysteries of the Arabian Knights. In the lecture, the chess problems start at 9:56, 33:39, and 45:40, with a fourth one toward the end. (The accompanying text was auto-generated by Webex, and is pretty funny: "chess problems" became "just problems" or "chest problems," etc. Not sure how to turn it off though.) I recommend watching at 1.25x speed though (or even faster) because I talked quite slowly that day.
Material from CAV 2021 tutorial ``Introduction to Algebraic Program Analysis'' (Z. Kincaid and T. Reps):
- Part 1 (Kincaid)
- Part 2 (Kincaid)
- Part 3 (Reps)
- Part 4 (Kincaid)
Reps interview for People of Programming Languages (2018)
The Reps At Sixty Workshop was held in Edinburgh, UK on September 11, 2016.
- Slides for most of the talks given at the workshop are now available on thewebsite.
- Some post-workshop reflections about (i) my work on machine-code analysis, and (ii) differences between academic and industry research are available here.
Information about the life of Susan Horwitz (1955-2014) can be found here.
Raghavan Komondoor has made available the software for detecting clones in C code that he developed as part of his Ph.D. dissertation.
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]
  was selected for inclusion in a special SIGPLAN collection of the 50 most influential papers from the SIGPLAN Conference on Programming Language Design and Implementation from 1979 to 1999:
- 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);ACM Author-Izer Link.]
  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;ACM Author-Izer Link.]

[Back to the Table of Contents]

Personnel

Faculty

Former Students, Post-Doctoral Associates, Staff, and Visitors

Matthew Amodio, 2017
Tycho Andersen, MS 2011
Min Thu Aung, MS 2012
Gogul Balakrishnan (Google), Ph.D. 2007
Thomas Ball (Microsoft Research, Redmond, WA), Ph.D. 1993
Victor Barger
Samuel Bates
David Binkley (Loyola College, Baltimore, MD), Ph.D. 1991
Jason Breck, (Google) Ph.D. 2020
Thomas Bricker
David Bingham Brown, Ph.D. 2020
Amanda Burton, MS 2010
Jiazhen Cai (NYU), Visitor 1990-91
John Cyphert, Ph.D. 2023
Manuvir Das (EMC), Ph.D. 1998
Evan Driscoll (GrammaTech, Inc.), Ph.D. 2013.
Matt Elder (Google), MS
Ben Farley, MS 2012
Denis Gopan (GrammaTech, Inc.), Ph.D. 2007
William Harris (Georgia Tech.), Ph.D. 2014
Beck Hasti (Univ. of Wisconsin), MS 1995
Jordan Henkel, Ph.D. 2022
Julien Henry (GrammaTech, Inc.), Visitor 2016-16
Neil Immerman (Univ. of Massachusetts), Visitor 2004-05
Bertrand Jeannet (IRISA), Visitor Mar. - June, 2003
Rich Joiner (Synopsys)
Nick Kidd (Google, Madison, WI), Ph.D. 2009
Raghavan Komondoor (Indian Institute of Science [IISc], Bangalore, India), Ph.D. 2003
Akash Lal (Microsoft Research India, Bangalore, India), Ph.D. 2009
Junghee Lim (GrammaTech, Inc.), Ph.D. 2011
Alexey Loginov (GrammaTech, Inc.), Ph.D. 2006
David Melski (GrammaTech, Inc.), Ph.D. 2002
Anne Mulhern
Lena Olson
Robert Paige (NYU), Visitor, 1990-91
Phil Pfeiffer (East Tennessee State University, Johnson City, TN), Ph.D. 1991
Prathmesh Prabhu, MS 2012
Jan Prins (University of North Carolina, Chapel Hill, NC), Visitor 1986-87
G. Ramalingam (Microsoft Research India, Bangalore, India), Ph.D. 1993
Genevive Rosay (retired; formerly GrammaTech, Inc.)
Mooly Sagiv (Tel-Aviv University, Israel), Visitor 1994-95
Stefan Schwoon (ENS Cachan, France), Visitor Feb. - Mar., 2003
Rathijit Sen
Tushar Sharma, Ph.D. 2017
Mike Siff (Sarah Lawrence College, Bronxville, NY), Ph.D. 1998
Meghana Aparna Sistla, (Indian Institute of Technology Madras), Visitor, May - July 2018
Venkatesh Srinivasan (Google, Mountain View), Ph.D. 2017
Aditya Thakur (Google, Mountain View), Ph.D. 2014
Emma Turetsky GrammaTech, Inc.
Zhichen Xu (Yahoo! Inc.), Ph.D. 2000
Mike Vaughn, Ph.D. 2024
Di Wang (Peking University), Visitor, June - August 2016.
Wuu Yang (National Chiao-Tung University, Hsinchu, Taiwan), Ph.D. 1990
Suan Hsi Yong (GrammaTech, Inc.), Ph.D. 2004
Xusheng Zhi, (Peking University), Visitor, January - July 2024
Zirui Zhou (Peking University), Visitor, July - September 2024
[Back to the Table of Contents]

Categorized Index to Project Publications

Program Slicing, Differencing, Merging, etc.

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

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

``Compositional recurrence analysis revisited''
``Newtonian program analysis via tensor product'' (also ``POPL16'')
``Improving pushdown system model checking''
``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 Table of Contents]

Alias Analysis, Pointer Analysis, and Shape Analysis

``Statically inferring complex heap, array, and numeric invariants''
``Finite differencing of logical formulas for static analysis'' (also ``Finite differencing of logical formulas for static analysis'', ESOP 2003)
``A relational approach to interprocedural shape analysis'' (also ``A relational approach to interprocedural shape analysis'', SAS 2004)
``Refinement-based verification for possibly-cyclic lists''
``Refinement-based program verification via three-valued-logic analysis''
``Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm''
``Recency-abstraction for heap-allocated storage''
``Automatic verification of strongly dynamic software systems''
``A relational abstraction for functions''
``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''
``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''
``Parametric shape analysis via 3-valued logic''
``On the non-approximability of points-to analysis''
``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)
``Fast and accurate flow-insensitive points-to analysis''
``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''
``On the adequacy of dependence-based representations for programs with heaps''
``Dependence-based representations for programs with reference variables''
``Dependence analysis for pointer variables''

Ph.D. Dissertations

``Numeric program analysis techniques with applications to array analysis and library summarization'' (Gopan thesis)
``Refinement-based program verification via three-valued-logic analysis'' (Loginov thesis)
``Dependence-based representations for programs with reference variables'' (Pfeiffer thesis)
[Back to the Table of Contents]

Analysis of Multi-Threaded Programs

``Verifying concurrent programs via bounded context-switching and induction''
``ConSeq: Detecting concurrency bugs through sequential errors''
``DIFC programs by automatic instrumentation''
``A decision procedure for detecting atomicity violations for communicating processes with locks'', STTT 11
(also ``A decision procedure for detecting atomicity violations for communicating processes with locks'', SPIN 09)
``Verifying information flow over unbounded processes''
``Reducing concurrent analysis under a context bound to sequential analysis'', FMSD 09
(also ``Reducing concurrent analysis under a context bound to sequential analysis'', CAV 08)
``Finding concurrency-related bugs using random isolation''
``Interprocedural analysis of concurrent programs under a context bound''
``Verifying concurrent message-passing C programs with recursive calls''
``Verifying temporal heap properties specified via evolution logic''

Ph.D. Dissertations

``Static verification of data-consistency properties'' (Kidd thesis)
``Interprocedural analysis and the verification of concurrent programs'' (Lal thesis)
[Back to the top]

Symbolic Abstraction and Decision Procedures

``Through the lens of abstraction''
``Satisfiability modulo abstraction for separation logic with linked lists''
``PostHat and all that: Automating abstract interpretation''
``Bilateral algorithms for symbolic abstraction''
``A generalization of Staalmarck's method''
``A method for symbolic computation of abstract operations''
``Symbolic implementation of the best transformer''
``Symbolically computing most-precise abstract operations for shape analysis''

Ph.D. Dissertations

``Symbolic abstraction: Algorithms and applications'' (Thakur thesis)
[Back to the top]

Path Problems

Context-Free-Language Reachability

``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''

Ph.D. Dissertations

``Interprocedural path profiling and the interprocedural express-lane transformation'' (Melski thesis)
``Bounded Incremental Computation'' (Ramalingam thesis)
``Multi-procedure program integration'' (Binkley thesis)
[Back to the Table of Contents]

Model Checking

``A decision procedure for detecting atomicity violations for communicating processes with locks'' (Journal version)
``Reducing concurrent analysis under a context bound to sequential analysis'' (Journal version)
``Finding concurrency-related bugs using random isolation''
``Reducing concurrent analysis under a context bound to sequential analysis''
``Interprocedural analysis of concurrent programs under a context bound''
``Advanced querying for property checking''
``Abstract error projection''
``Improving pushdown system model checking''
``Weighted pushdown systems and trust-management systems''
``Verifying concurrent message-passing C programs with recursive calls''
``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''

Software

``WPDS++: A C++ Library for Weighted Pushdown Systems''
``WALi: The Weighted Automaton Library''
``OpenNWA: A Nested-Word Automaton Library''

Ph.D. Dissertations

``Checking format compatibility of programs using automata'' (Driscoll thesis)
``Static verification of data-consistency properties'' (Kidd thesis)
``Interprocedural analysis and the verification of concurrent programs'' (Lal thesis)
[Back to the Table of Contents]

Computer Security

``Efficient runtime enforcement techniques for policy weaving''
``Declarative, temporal, and practical programming with capabilities''
``TSL: A system for generating abstract interpreters and its application to machine-code analysis''
``DIFC programs by automatic instrumentation''
``DIVINE: DIscovering Variables IN Executables''
``Reducing the dependence of SPKI/SDSI on PKI''
``Weighted pushdown systems and trust-management systems''
``Intermediate-representation recovery from low-level code''
``A next-generation platform for analyzing executables''
``WYSINWYX: What You See Is Not What You eXecute''
``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

``Secure programming via game-based synthesis'' (Harris thesis)
``Transformer Specification Language: A system for generating analyzers and its applications'' (Lim thesis)
``WYSINWYX: What You See Is Not What You eXecute'' (Balakrishnan thesis)
``Safety-checking of machine code'' (Xu thesis)
[Back to the Table of Contents]

Quantum Computing

``Scalable equivalence checking and verification of shallow quantum circuits''
``Weighted context-free-language ordered binary decision diagrams''
``CFLOBDDs: Context-free-language ordered binary decision diagrams''
``Symbolic quantum simulation with Quasimodo''
[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 Table of Contents]

Computational Differentiation and Computational Divided Differencing

``Algorithmic differencing''
``Computational divided differencing and divided-difference arithmetics''
``Computational divided differencing and divided-difference arithmetics''
[Back to the Table of Contents]

Clone Detection

``Effective, automatic procedure extraction''
``Using slicing to identify duplication in source code''
``Tool Demonstration: Finding duplicated code using program dependences''
``Semantics-preserving procedure extraction''

Software

``Software for detecting clones in C code''

Ph.D. Dissertations

``Automated duplicated-code detection and procedure extraction''
[Back to the Table of Contents]

Miscellaneous

```Maximal-munch' tokenization in linear time''
[Back to the Table of Contents]

Project Bibliography

Books

Datta, A., Jha, S., Li, N., Melski, D., and Reps, T., Analysis Techniques for Information Security. Synthesis Lectures on Information Security, Privacy, and Trust, Morgan & Claypool Publishers, 2010. [Access via digital object identifier.]
Reps, T. and Teitelbaum, T., The Synthesizer Generator: A System for Constructing Language-Based Editors. Springer-Verlag, New York, NY, 1988. [abstract;Amazon.com;Access via SpringerLink.]
Reps, T. and Teitelbaum, T., The Synthesizer Generator Reference Manual: Third Edition. Springer-Verlag, New York, NY, 1988. [Access via SpringerLink.]
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 1983ACM Doctoral Dissertation Award.)**[abstract;Amazon.com;Access via IEEEXplore.]
[Back to the top]

Journal Publications

Kalita, P.K., Reps, T., and Roy, S.,Automated abstract transformer synthesis for reduced product domains. In ACM Trans. on Softw. Eng. and Methodology (TOSEM) (2025). DOI: 10.1145/3733716 [ACM Link.]
Murphy, C., Johnson, K., Reps, T., and D'Antoni, L.,Verifying solutions to semantics-guided synthesis problems. To appear in PACMPL 9(PLDI) (2025).
Kim, J., Nagy, S., Reps, T., and D'Antoni, L.,Semantics of sets of programs. In PACMPL 9(OOPSLA1) (2025). DOI: 10.1145/3720515 [ACM Link.]
Zhi, X., and Reps, T.W.,Polynomial bounds of CFLOBDDs against BDDs. In ACM Trans. on Program. Lang. and Syst. (TOPLAS) 47(2): 4:1--4:36 (2025). DOI: 10.1145/3716313. [ACM Link.]
Sistla, M., Chaudhuri, S., and Reps, T.,Weighted context-free-language ordered binary decision diagrams. In PACMPL 8(OOPSLA2), 1390-1419 (2024). [ACM Link.]
Johnson, K.J.C., Krishnan, R., Reps, T., and D'Antoni, L.,Automating pruning in top-down enumeration for program synthesis problems with monotonic semantics. In PACMPL 8(OOPSLA2), 935-961 (2024). [ACM Link.]
Liu, J., Murphy, C., Grover, A., Johnson, K., Reps, T., D'Antoni, L.,Synthesizing formal semantics from executable interpreters. In PACMPL 8(OOPSLA2), 362-388 (2024). [ACM Link.]
Nagy, S., Kim, J., Reps, T., and D'Antoni, L.,Automating unrealizability logic: Hoare-style proof synthesis for infinite sets of programs. In PACMPL 8(OOPSLA2), 113-139 (2024). [ACM Link.]
Wang, D. and Reps, T.,Newtonian program analysis of probabilistic programs. In PACMPL 8(OOPSLA1) (2024), 305-333. [ACM Link.]
Sistla, M., Chaudhuri, S., and Reps, T.,CFLOBDDs: Context-free-language ordered binary decision diagrams. In ACM Trans. on Program. Lang. and Syst. (TOPLAS) 46(2): 7:1--7:82 (2024). (Also presented as a journal-first paper at the ACM Conference on Programming Language Design and Implementation (PLDI), 2024.) [abstract;ACM Link.PDF;slides.] (Extended version: arXiv:2211.06818, Nov. 2022; revised May 2024.)
Park, K., D'Antoni, L., and Reps, T.,Synthesizing specifications. In PACMPL 7(OOPSLA2), 1787-1816 (2023).ACM Link.
Li, Y., Zhang, Q., and Reps, T.,Single-source-single-target interleaved-Dyck reachability via integer linear programming. In PACMPL (POPL) (2023). [PDF.]
Kim, J., D'Antoni, L., and Reps, T.,Unrealizability logic. In PACMPL (POPL) (2023). [PDF,Talk.]
Kalita, P., Muduli, S., D'Antoni, L., Reps, T., and Roy, S.,Synthesizing abstract transformers. In PACMPL (OOPSLA), Dec. 2022. [PDF.]
Li, Y., Zhang, Q., and Reps, T.,Fast graph simplification for interleaved Dyck-reachability. In ACM Trans. on Program. Lang. and Syst. (TOPLAS) 44(2): 11:1--11:28 (2022). [ACM Link.]
Kim, J., Hu, Q., D'Antoni, L., and Reps, T.,Semantics-guided synthesis. In PACMPL 5(POPL) (2021). [ACM Author-Izer Link.]
Li, Y., Zhang, Q., and Reps, T.,On the complexity of bidirected interleaved Dyck-reachability. In PACMPL 5(POPL) (2021). [ACM Author-Izer Link.]
Liu, P., Wahl, T., and Reps, T.,Interprocedural context-unbounded program analysis using observation sequences. In ACM Trans. on Program. Lang. and Syst. 42(4): 16:1-16:34 (2021). [ACM Author-Izer Link.]
Cyphert, J., Breck, J., Kincaid, Z., and Reps, T.,Refinement of path expressions for static analysis. In PACMPL 3(POPL) (2019). [abstract;PDF;ACM Author-Izer Link.]
Kincaid, Z., Breck, J., Cyphert, J., and Reps, T.,Closed forms for numerical loops. In PACMPL 3(POPL) (2019). [abstract;PDF;ACM Author-Izer Link.]
Sharma, T. and Reps, T.,A new abstraction framework for affine transformers. In Formal Methods in System Design (FMSD). [abstract;PDF;Springer page.]
Kincaid, Z., Cyphert, J., Breck, J., and Reps, T.,Non-linear reasoning for invariant synthesis. In PACMPL 2(POPL): 54:1-54:33 (2018). [abstract;PDF;ACM Author-Izer Link;Slides]
Harris, W., Jha, S., Reps, T., and Seshia, S.,Program synthesis for interactive-security systems. In Formal Methods in System Design (FMSD) 51(2): 362-394 (2017). [abstract;Springer page.]
Srinivasan, V., Vartanian, A., and Reps, T.,Model-assisted machine-code synthesis. In PACMPL 1(OOPSLA): 61:1-61:26 (2017). [abstract;PDF;ACM Author-Izer Link;slides]
Reps, T., Turetsky, E., and Prabhu, P.,Newtonian program analysis via tensor product. In ACM Trans. on Program. Lang. and Syst. (TOPLAS) 39(2): 9:1-9:72 (2017). [abstract;PDF;slides;POPL 2016 talk;ACM Author-Izer Link.]
Thakur, A., Lal, A., Lim, J., and Reps, T.,PostHat and all that: Automating abstract interpretation. In Electr. Notes Theor. Comput. Sci. 311 15-32 (2015). [abstract;PDF.]
Elder, M., Lim, J., Sharma, T., Andersen, T., and Reps, T.,Abstract domains of affine relations. In ACM Trans. on Program. Lang. and Syst. (TOPLAS) 36(4): 11:1-11:73 (2014). [abstract;PDF;ACM Author-Izer Link;slides.]
Aung, M., Horwitz, S., Joiner, R., and Reps, T.,Specialization slicing. In ACM Trans. on Program. Lang. and Syst. (TOPLAS) 36(2): 5:1-5:67 (2014). (Also presented as a journal-first paper at the ACM Conference on Programming Language Design and Implementation (PLDI), 2014.) [abstract;PDF;slides;ACM Author-Izer Link.]
Lim, J. and Reps. T.,TSL: A system for generating abstract interpreters and its application to machine-code analysis. In ACM Trans. on Program. Lang. and Syst. (TOPLAS) 35(1): 4:1-4:59 (2013). [abstract;PDF;ACM Author-Izer Link.]http://doi.acm.org/10.1145/2450136.2450139.
Zhang, W., Sun, C., Lim, J., Lu, S., and Reps, T.,ConMem: Detecting crash-triggering concurrency bugs through an effect-oriented approach. In ACM Transactions on Software Engineering and Methodology (TOSEM) 22(2): 10:1-10:33 (2013). [abstract;ACM Author-Izer Link.]
Kidd, N., Reps, T., Dolby, J., and Vaziri, M.,Finding concurrency-related bugs using random isolation. In Int. Journal on Software Tools for Technology Transfer 13, 6 (2011), 495-518. [abstract;PDF;DOI;(c) Springer-Verlag]
Kidd, N., Lammich, P., Touili, T., and Reps, T.,A decision procedure for detecting atomicity violations for communicating processes with locks. In Int. Journal on Software Tools for Technology Transfer 13, 1 (2011), 37-60. [abstract;PDF;DOI;(c) Springer-Verlag]
Lim, J., Lal, A., and Reps, T.,Symbolic analysis via semantic reinterpretation. In Int. Journal on Software Tools for Technology Transfer 13, 1 (2011), 61-87. [abstract;PDF;DOI;(c) Springer-Verlag]
Elder, M., Gopan, D., and Reps, T.,View-augmented abstractions. In Electr. Notes Theor. Comput. Sci. 267, 1 (2010), 43-57. [abstract;PDF.]
Reps, T., Sagiv, M., and Loginov, A.,Finite differencing of logical formulas for static analysis. In ACM Trans. on Program. Lang. and Syst. (TOPLAS) 32(6): 24:1-24:55 (2010). [abstract;PDF;ACM Author-Izer Link.]http://doi.acm.org/10.1145/1749608.1749613.
Balakrishnan, G. and Reps, T.,WYSINWYX: What You See Is Not What You eXecute. In ACM Trans. on Program. Lang. and Syst. (TOPLAS) 32(6): 23:1-23:84 (2010). [abstract;PDF;ACM Author-Izer Link.]http://doi.acm.org/10.1145/1749608.1749612.
Jeannet, B., Loginov, A., Reps, T., and Sagiv, M.,A relational approach to interprocedural shape analysis. In ACM Trans. on Program. Lang. and Syst. (TOPLAS) 32(2): 5:1-5:52 (2010). [abstract;PDF;ACM Author-Izer Link.]http://doi.acm.org/10.1145/1667048.1667050.
Lal, A. and Reps, T.,Reducing concurrent analysis under a context bound to sequential analysis. In Formal Methods in System Design 35, 1 (2009), 73-97. [abstract;PDF;(c) Springer-Verlag]
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. In Logical Methods in Computer Science 5, 2 (2009). [abstract;PostScript;PDF.]
Yorshz, G., Reps, T., Sagiv, M., and Wilhelm, R.,Logical characterizations of heap abstractions. In ACM Transactions on Computational Logic 8(1): 5:1-5:27 (2007). [abstract;PostScript;PDF;ACM Author-Izer Link.]
Yahav, E., Reps, T., Sagiv, M., and Wilhelm, R.,Verifying temporal heap properties specified via evolution logic.Logic Journal of the IGPL 14, 5 (Oct. 2006), 755-784. [abstract;PDF.]
Reps, T., Schwoon, S., Jha, S., and Melski, D.,Weighted pushdown systems and their application to interprocedural dataflow analysis.Science of Computer Programming 58, 1-2 (Oct. 2005), 206-263. [abstract;PostScript; PDF.]
Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., and Yannakakis, M.,Analysis of recursive state machines. In ACM Trans. on Program. Lang. and Syst. (TOPLAS) 27, 4 (2005), 786-818. [abstract;ACM Author-Izer Link.]
Yorsh, G., Skidanov, A., Reps, T., and Sagiv, M.,Assume/guarantee reasoning for heap-manipulating programs. In Electronic Notes in Theoretical Computer Science 131, 24 (May 2005), 125-138. [abstract;PostScript;PDF]
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. [abstract;paper, via IEEE Explore.]
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;ACM Author-Izer Link; talk: Powerpoint]
Chakaravarthy, V. and Horwitz, S., On the non-approximability of points-to analysis.Acta Informatica 38, 8 (June 2002).
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;ACM Author-Izer Link.]
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;paper, via IEEE Explore.]
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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
S. Horwitz,Precise flow-insensitive may-alias analysis is NP-hard._ACM Transactions on Programming Languages and Systems_Vol 19 No 1, (January 1997), 1-6.toplas97a.ps
Sagiv, M., Reps, T., and Horwitz, S.,Precise interprocedural dataflow analysis with applications to constant propagation.Theoretical Computer Science 167 (1996), 131-170. [abstract;PDF]
Reps, T.,On the sequential nature of interprocedural program-analysis problems.Acta Informatica 33 (1996), 739-757. [abstract;paper]
Binkley, D., Horwitz, S., and Reps, T.,Program integration for languages with procedure calls.ACM Transactions on Software Engineering and Methodology (TOSEM) 4, 1 (January 1995), pp. 3-35. [abstract;paper;ACM Author-Izer Link.]
Yang, W., Horwitz, S., and Reps, T.,A program integration algorithm that accommodates semantics-preserving transformations.ACM Transactions on Software Engineering and Methodology (TOSEM) 1, 3 (July 1992), 310-354. [abstract;ACM Author-Izer Link.]
Yang, W.,Identifying syntactic differences between two programs.Software - Practice & Experience 21, 7 (July 1991), pp. 739-755.
Reps, T.,Algebraic properties of program integration.Science of Computer Programming 17 (1991), 139-215. [abstract;PS;PDF]
Horwitz, S. and Reps, T.,Efficient comparison of program slices.Acta Informatica 28 (1991), 713-732. [PDF.]
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;ACM Author-Izer Link.]
Horwitz, S., Prins, J., and Reps, T.,Integrating noninterfering versions of programs.ACM Transactions on Programming Languages and Systems 11, 3 (July 1989), 345-387. [abstract;paper;ACM Author-Izer Link.]
Reps, T.Incremental evaluation for attribute grammars with unrestricted movement between tree modifications.Acta Informatica 25 (1988), 155-178. [PDF.]
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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.] Corrigenda, ACM Transactions on Programming Languages and Systems 5, 4 (October 1983). [ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
[Back to the Table of Contents]

Invited Papers

Kincaid, Z., Reps, T.W., and Cyphert, J.,Algebraic program analysis (Invited tutorial). In Computer Aided Verification (CAV), Part I, LNCS 12759, Springer, 2021. [abstract;PDF.]
D'Antoni, L., Hu, Q., Kim, J., and Reps, T.W.,Programmable program synthesis. In Computer Aided Verification (CAV), Part I, LNCS 12759, Springer, 2021. [abstract;PDF.]
Reps, T.,Program analyses using Newton's method. In Proc. Int. Conf. on NETworked sYStems (NETYS), May 2018. [abstract;PDF;slides;(c) Springer-Verlag]
Reps, T. and Thakur, A.,Automating abstract interpretation. In Proc. Verification, Model Checking, and Abstract Interpretation (VMCAI), Jan. 2016. [abstract;PDF;(c) Springer-Verlag;video recording;slides]
McCloskey, B., Reps, T., and Sagiv, M.,Statically inferring complex heap, array, and numeric invariants. In Proc. Static Analysis Symposium (SAS), Sept. 2010. [abstract;PDF;(c) Springer-Verlag]
Reps, T., Lim, J., Thakur, A., Balakrishnan, G., and Lal, A.,There's plenty of room at the bottom: Analyzing and verifying machine code (Invited tutorial). In Proc. Computer Aided Verification, 2010. [abstract;PDF;(c) Springer-Verlag; slides: Powerpoint]
Reps, T. and Balakrishnan, G.,Improved memory-access analysis for x86 executables. (Paper accompanying ``unifying'' invited talk at ETAPS 2008.) In Proc. Int. Conf. on Compiler Construction, April 2008. [abstract;PDF;(c) Springer-Verlag]
Reps, T., Lal, A., and Kidd, N.,Program analysis using weighted pushdown systems. In Proc. 27th Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), (New Delhi, India, Dec. 12-14, 2007). [abstract;PDF;(c) Springer-Verlag; talk: Powerpoint.]
Balakrishnan, G., and Reps, T.,DIVINE: DIscovering Variables IN Executables. In Proc. Verification, Model Checking, and Abstract Interpretation (VMCAI), (Nice, France, Jan. 14-16, 2007). [abstract;PDF;(c) Springer-Verlag.]
Jha, S., Schwoon, S., Wang, H., and Reps, T.,Weighted pushdown systems and trust-management systems. In Proc. TACAS, (Vienna, Austria, Mar. 25 - Apr. 2, 2006), Springer-Verlag, New York, NY, 2006. [abstract;PDF;(c) Springer-Verlag.]
Reps, T., Balakrishnan, G., and Lim, J.Intermediate-representation recovery from low-level code. In Proc. Workshop on Partial Evaluation and Program Manipulation (PEPM), (Charleston, SC, Jan. 9-10, 2006). [abstract;PostScript;PDF;ACM Author-Izer Link.]
Reps, T., Balakrishnan, G., Lim, J., and Teitelbaum, T.,A next-generation platform for analyzing executables. In Proc. 3rd Asian Symposium on Programming Languages and Systems, (Tsukuba, Japan, Nov. 3-5, 2005), Springer-Verlag, New York, NY, 2005. [abstract;PostScript;PDF;(c) Springer-Verlag.]
Reps, T., Sagiv, M., and Wilhelm, R.,Static program analysis via 3-valued logic. In Proc. Int. Conf. on Computer-Aided Verification, Springer-Verlag, New York, NY, 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. Facius (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;Springer Link.]
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;ACM Author-Izer Link.]
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. [PDF.]
[Back to the Table of Contents]

Book Chapters

Kreiker, J., Reps, T., Rinetzky, N., Sagiv, M., Wilhelm, R., and Yahav, E.,Interprocedural shape analysis for effectively cutpoint-free programs. In Programming Logics: Essays in Memory of Harald Ganzinger, LNCS 7797, Springer, 2013.
Ramalingam, G. and Reps, T.,Semantics of program representation graphs. In Semantics to Computer Science: Essays in Honour of Gilles Kahn, Y. Bertot, G. Huet, J.-J. Levy, and G. Plotkin (eds.), Cambridge University Press, 2009.
Reps, T., Sagiv, M., and Bauer, J.,An Appreciation of the Work of Reinhard Wilhelm. In Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm, Lecture Notes in Computer Science, Vol. 4444, Springer-Verlag, 2007. [PDF]
Reps, T., Sagiv, M., and Wilhelm, R.,Shape analysis and applications. Chapter 12 in The Compiler Design Handbook: Optimizations and Machine Code Generation, 2nd Edition, CRC Press, 2007.
Clarke, E., Kroening, D., and Reps, T.,Static analysis to enhance the power of model checking for concurrent software. In Department of Defense Sponsored Information Security Research: New Methods for Protecting Against Cyber Threats, Wiley, 2007, 349-360.
Balakrishnan, G., Christodorescu, M., Ganapathy, V., Giffin, J.T., Rubin, S., Wang, H., Jha, S., Miller, B.P., and Reps, T.,Analysis of COTS for Security Vulnerability Remediation In Department of Defense Sponsored Information Security Research: New Methods for Protecting Against Cyber Threats, Wiley, 2007, 375-380.
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-253.
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 Table of Contents]

Reprinted in Collections

Reps, T.W. and Rall, L.B., Computational divided differencing and divided-difference arithmetics,In Automatic Program Development: A Tribute to Robert Paige, Danvy, O., Mairson, H., Henglein, F., and Pettorossi, A. (Eds.), Springer Verlag, 2008.
Revised version of Reps, T.W. and Rall, L.B., Computational divided differencing and divided-difference arithmetics.Higher-Order and Symbolic Computation 16, 1-2 (June 2003).
Loginov, A., Reps, T., and Sagiv, M., Abstraction refinement via inductive learning,In Department of Defense Sponsored Information Security Research: New Methods for Protecting Against Cyber Threats, Wiley, 2007, 361-374.
Reprinted from Proc. Computer-Aided Verification, 2005.
Reps, T., Balakrishnan, G., Lim, J., and Teitelbaum, T., A next-generation platform for analyzing executables. In Malware Detection, Advances in Information Security Series, Vol. 27, M. Christodorescu, S. Jha, D. Maughan, D. Song, and C. Wang (eds.), Springer-Verlag, 2006, pp. 43-61.
Reprinted from Proc. 3rd Asian Symposium on Programming Languages and Systems, (Tsukuba, Japan, Nov. 3-5, 2005).
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);ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
Horwitz, S., Prins, J., and Reps, T.,Integrating noninterfering 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;ACM Author-Izer Link.]
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. [PDF.]
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;ACM Author-Izer Link.]
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. [ACM Author-Izer Link.]

[Back to the Table of Contents]

Edited Books

Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm,T. Reps, M. Sagiv, and J. Bauer (eds.), Lecture Notes in Computer Science, Vol. 4444, Springer-Verlag, 2007. [For information, click here; or access the online versionhere.]
Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Boston, Massachusetts, USA, January 19-21, 2000,M.N. Wegman and T.W. Reps (eds.) ACM, 2000. [Link via ACM Digital Library.]

[Back to the Table of Contents]

Conference and Refereed Workshop Publications

Kalita, P.K., Reps, T., and Roy, S.,Synthesizing abstract transformers for reduced-product domains. In Static Analysis Symposium (SAS), 2024. [Springer Link.]
Jain, A., Chaudhuri, S., Reps, T.W., and Jermaine, C.M., Prompt tuning strikes back: Customizing foundation models with low-rank prompt adaptation. In Conference on Neural Information Processing Systems (NeurIPS), 2024. [Link to paper.]
Johnson, K.J.C., Reynolds, A., Reps, T., and D'Antoni, L.,The SemGuS Toolkit. In Computer Aided Verification (CAV), 2024 [Springer Link.]
Park, K., Johnson, K.J.C., D'Antoni, L. and Reps, T.,Modular system synthesis. In Formal Methods in Computer-Aided Design (FMCAD), 2023. [[PDF]([<A HREF=).]
Sistla, M., Chaudhuri, S., and Reps, T.,Symbolic quantum simulation with Quasimodo. In Computer Aided Verification (CAV), 2023. [Springer Link.]
Alhanahnah, M., Jain, R., Rastogi, V. Jha, S., and Reps, T.,Lightweight, multi-stage, compiler-assisted application specialization. In 7th IEEE European Symposium on Security and Privacy, June 2022. [IEEE Link.]
Henkel, J.,* Ramakrishnan, G.,* Wang, Z., Albarghouthi, A., Jha, S., and Reps, T.,Semantic robustness of models of source code. In 29th IEEE Int. Conf. on Software Analysis, Evolution and Reengineering (SANER), March 2022. (``*'' denotes equal contributions.) [IEEE Link.]
Mukherjee, R., Wen, Y., Chaudhari, D., Reps, T., Chaudhuri, S., and Jermaine, C.,Neural program generation modulo static analysis. In Conference on Neural Information Processing Systems (NeurIPS), 2021. (Spotlight presentation). [Link to paper.]
Hu, Q., Cyphert, J., D'Antoni, L., and Reps, T.W.,Synthesis with asymptotic resource bounds. In Computer Aided Verification (CAV), Part I, LNCS 12759, Springer, 2021. [PDF.]
Henkel, J., Silva, D., Teixeira, L., d'Amorim, M., and Reps, T.W.,Shipwright: A human-in-the-loop system for Dockerfile repair. In Proc. Int. Conf. on Software Engineering (ICSE), 2021. [IEEE Link.]
Wang, D., Hoffmann, J., and Reps, T.,Central moment analysis for cost accumulators in probabilistic programs. In ACM Conference on Programming Language Design and Implementation (PLDI), 2021. [ACM Author-Izer Link.]
Wang, D., Hoffmann, J., and Reps, T.,Sound probabilistic inference via guide types. in ACM Conference on Programming Language Design and Implementation (PLDI), 2021. [ACM Author-Izer Link.]
Henkel, J., Bird, C., Lahiri, S.K., and Reps, T.,A dataset of Dockerfiles. In Mining Software Repositories (Data Showcase Track), 2020. [ACM Author-Izer Link.]
Henkel, J., Bird, C., Lahiri, S.K., and Reps, T.,Learning from, understanding, and supporting DevOps artifacts for Docker. In Proc. Int. Conf. on Software Engineering (ICSE), 2020. [abstract;PDF;ACM Author-Izer Link.]
Hu, Q., Cyphert, J., D'Antoni, L., and Reps, T.,Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems. In Proc. ACM Conference on Programming Language Design and Implementation (PLDI), 2020. [abstract;PDF;ACM Author-Izer Link;corrigenda.]
Li, Y., Zhang, Q., and Reps, T.,Fast graph simplification for interleaved Dyck-reachability. In Proc. ACM Conference on Programming Language Design and Implementation (PLDI), 2020.**(2020 PLDI Distinguished Paper.)**[abstract;PDF;ACM Author-Izer Link.]
Breck, J., Cyphert, J., Kincaid, Z., and Reps, T.,Templates and recurrences: Better together. In Proc. ACM Conference on Programming Language Design and Implementation (PLDI), 2020. [abstract;PDF;ACM Author-Izer Link.]
Hu, Q., Breck, J., Cyphert, J., D'Antoni, L., and Reps, T.,Proving unrealizability for syntax-guided synthesis. In Computer Aided Verification (CAV), 2019. [PDF.]
Wang, D., Hoffmann, J., and Reps, T.,A denotational semantics for low-level probabilistic programs with nondeterminism. In Mathematical Foundations of Programming Semantics (MFPS), 2019. [PDF.]
Henkel, J., Lahiri, S., Liblit, B., and Reps, T.,Code vectors: Understanding programs through embedded abstracted symbolic traces. In ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2018. [abstract;paper (PDF);ACM Author-Izer Link.]
Wang, D., Hoffmann, J., and Reps, T.,PMAF: An algebraic framework for static analysis of probabilistic programs. In Proc. ACM Conference on Programming Language Design and Implementation (PLDI), 2018. [abstract;paper (PDF);ACM Author-Izer Link;slides (PDF).]
Sharma, T. and Reps, T.,A new abstraction framework for affine transformers. In Proc. Static Analysis Symposium (SAS), 2017. [abstract;PDF;extended version with proofs;slides;(c) Springer-Verlag]
Brown, D.B., Vaughn, M., Liblit, B., and Reps, T.,The care and feeding of wild-caught mutants. In Proc. Joint Meeting of the European Software Eng. Conf. and the ACM SIGSOFT Symp. on the Foundations of Software Engineering (ESEC/FSE), 2017. [abstract;PDF;ACM Author-Izer Link.]
Carbonneaux, Q., Hoffmann, J., Reps, T., and Shao, Z.,Automated resource analysis with Coq proof objects. In Proc. Int. Conf. on Computer Aided Verifications (CAV), 2017. [abstract;PDF;(c) Springer-Verlag]
Kincaid, Z., Breck, J., Forouhi Boroujeni, A., and Reps, T.,Compositional recurrence analysis revisited. In Proc. ACM Conference on Programming Language Design and Implementation (PLDI), 2017. [abstract;PDF;ACM Author-Izer Link;Slides]
Extended version: TR-1840, Computer Sciences Department, University of Wisconsin, Madison, WI. Revised April 2017. [abstract;PDF]
Sharma, T. and Reps, T.,Sound bit-precise numerical domains. In Proc. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2017. [abstract;PDF]
Feng, Y., Martins, R., Wang, Y., Dillig, I., and Reps, T.W.,Component-based synthesis for complex APIs. In Proc. ACM Symposium on Principles of Programming Languages (POPL), 2017. [abstract;PDF;ACM Author-Izer Link.]
Srinivasan, V., Sharma, T., and Reps, T.,Speeding up machine-code synthesis. In Proc. ACM SIGPLAN Conf. on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH/OOPSLA), 2016. [abstract;PDF;ACM Author-Izer Link;slides]
Srinivasan, V. and Reps, T., An improved algorithm for slicing machine code. In Proc. ACM SIGPLAN Conf. on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH/OOPSLA), 2016. [abstract;PDF;ACM Author-Izer Link;slides]
Miné, A., Breck, J., and Reps, T.,An algorithm inspired by constraint solvers to infer inductive invariants in numeric programs. In Proc. European Symp. on Programming (ESOP), Apr. 2016. [abstract;PDF]
Reps, T., Turetsky, E., and Prabhu, P.,Newtonian program analysis via tensor product. In Conference Record of the ACM Symposium on Principles of Programming Languages (POPL), 2016. [abstract;conference version;ACM Author-Izer Link;journal version;slides;POPL 2016 talk]
Ohmann, P., Brown, D.B., Liblit, B., and Reps, T.,Recovering execution data from incomplete observations. In Proc. 13th International Workshop on Dynamic Analysis, (WODA), 2015. [ACM Author-Izer Link.]
Srinivasan, V. and Reps, T.,Partial evaluation of machine code. In Proc. ACM SIGPLAN Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH/OOPSLA), 2015. [abstract;conference version;ACM Author-Izer Link;extended version;slides]
Srinivasan, V. and Reps, T.,Synthesis of machine code from semantics. In Proc. ACM Conference on Programming Language Design and Implementation (PLDI), 2015. [abstract;PDF;ACM Author-Izer Link;slides]
Joiner, R., Reps, T., Jha, S., Dhawan, M., and Ganapathy, V.,Efficient runtime enforcement techniques for policy weaving. In Proc. Foundations of Software Engineering (FSE), 2014. [abstract;PDF;ACM Author-Izer Link]
Thakur, A., Breck, J., and Reps, T.,Satisfiability modulo abstraction for separation logic with linked lists. In Proc. Int. SPIN Symposium on Model Checking of Software (SPIN), 2014. [abstract;PDF;ACM Author-Izer Link;Powerpoint.]
Aung, M., Horwitz, S., Joiner, R., and Reps, T.,Specialization slicing. In Proc. ACM Conference on Programming Language Design and Implementation (PLDI), 2014. (Journal-first conference paper; see the TOPLAS 2014 paper.) [abstract;PDF;ACM Author-Izer Link.]
Itzhaky, S., N. Bjørner, Reps, T., Sagiv, M., and Thakur, A.,Property-directed shape analysis. In Proc. Computer-Aided Verification (CAV), 2014. [abstract;PDF;(c) Springer-Verlag]
Srinivasan, V. and Reps, T.,Recovery of class hierarchies and composition relationships from machine code. In Proc. Int. Conf. on Compiler Construction (CC), 2014. [abstract;PDF;slides](c) Springer-Verlag]
Harris, W.R., Jha, S., Reps, T., Anderson, J., and Watson, R.N.M.,Declarative, temporal, and practical programming with capabilities. In Proc. IEEE Symposium on Security and Privacy (SP), 2013. [abstract;PDF]
Thakur, A., Elder, M., and Reps, T.,Bilateral algorithms for symbolic abstraction. In Proc. Static Analysis Symposium (SAS), 2012. [abstract;PDF;(c) Springer-Verlag]
Thakur, A. and Reps, T.,A generalization of Staalmarck's method. In Proc. Static Analysis Symposium (SAS), 2012. [abstract;PDF; extended version: TR-1699r;(c) Springer-Verlag]
Harris, W.R., Jha, S., and Reps, T.,Secure programming via visibly pushdown safety games. In Proc. Computer-Aided Verification (CAV), 2012. [abstract;PDF;(c) Springer-Verlag]
Fredrikson, M., Joiner, R., Jha, S., Reps, T., Porras, P., Saïdi, H., and Yegneswaran, V.,Efficient runtime policy enforcement using counterexample-guided abstraction refinement. In Proc. Computer-Aided Verification (CAV), 2012. [abstract;PDF;(c) Springer-Verlag]
Thakur, A. and Reps, T.,A method for symbolic computation of abstract operations. In Proc. Computer-Aided Verification (CAV), 2012. [abstract;PDF;(c) Springer-Verlag]
Driscoll, E., Thakur, A., and Reps, T.,OpenNWA: A nested-word-automaton library (tool paper). In Proc. Computer-Aided Verification (CAV), 2012. [abstract;PDF;(c) Springer-Verlag]
Elder, M., Lim, J., Sharma, T., Andersen, T., and Reps, T.,Abstract domains of affine relations. In Proc. Static Analysis Symposium (SAS), 2011. [abstract;SAS 11 version;Extended version with proofs (TR-1691);slides;(c) Springer-Verlag]
Driscoll, E., Burton, A., and Reps, T.,Checking conformance of a producer and a consumer. In Proc. Found. of Software Engineering (FSE), 2011. [abstract;PDF;ACM Author-Izer Link.]
Zhang, W., Lim, J., Olichandran, R., Scherpelz, J., Jin, G., Lu, S., and Reps, T.,ConSeq: Detecting concurrency bugs through sequential errors. In Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2011. [abstract;PDF;ACM Author-Izer Link.]
Harris, W., Jha, S., and Reps, T.,DIFC programs by automatic instrumentation. In Proc. ACM Conf. on Computer and Communications Security (CCS), 2010. [abstract;PDF;ACM Author-Izer Link.]
Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., Andersen, T., and Reps, T.,Directed proof generation for machine code. In Proc. Computer-Aided Verification (CAV), 2010. [abstract;CAV 10 version;Extended version (TR-1669);(c) Springer-Verlag]
Harris, W., Kidd, N., Chaki, S., Jha, S., and Reps, T.,Verifying information flow over unbounded processes. In Proc. Int. Symp. on Formal Methods (FM), 2009. [abstract;PDF;(c) Springer-Verlag]
Kidd, N., Lammich, P., Touili, T., and Reps, T.,A decision procedure for detecting atomicity violations for communicating processes with locks. In Proc. SPIN Workshop, 2009. [abstract;PDF;(c) Springer-Verlag] (An extended version with proofs is availablehere.)
Lim, J., Lal, A., and Reps, T.,Symbolic analysis via semantic reinterpretation. In Proc. SPIN Workshop, 2009. [abstract;PDF;(c) Springer-Verlag]
Kidd, N., Reps, T., Dolby, J., and Vaziri, M.,Finding concurrency-related bugs using random isolation. In Proc. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2009. [abstract;PDF;(c) Springer-Verlag]
Lal, A. and Reps, T.,Reducing concurrent analysis under a context bound to sequential analysis. In Proc. Computer-Aided Verification (CAV), 2008. [abstract;PDF;(c) Springer-Verlag]
Lal, A. and Reps, T.,Solving multiple dataflow queries. In Proc. Static Analysis Symposium (SAS), July 2008. [abstract;PDF;(c) Springer-Verlag]
Kidd, N., Lal, A. and Reps, T.,Language strength reduction. In Proc. Static Analysis Symposium (SAS), July 2008. [abstract;PDF;(c) Springer-Verlag]
Lim, J. and Reps, T., A system for generating static analyzers for machine instructions. In Proc. Int. Conf. on Compiler Construction (CC), April 2008.**(Awarded the EAPLS Best Paper Award at ETAPS 2008.)**[abstract;PDF; slides: Powerpoint (12 MB);(c) Springer-Verlag]
Balakrishnan, G. and Reps, T.,Analyzing stripped device-driver executables. In Proc. TACAS, Springer-Verlag, New York, NY, April 2008. [abstract;PDF; slides: Powerpoint;(c) Springer-Verlag]
Lal, A., Touili, T., Kidd, N., and Reps, T.,Interprocedural analysis of concurrent programs under a context bound. In Proc. TACAS, Springer-Verlag, New York, NY, April 2008. [abstract;PDF;extended version with proofs and examples (TR-1598, CS Dept., Univ. of Wisconsin); slides: Powerpoint;(c) Springer-Verlag]
Lal, A., Kidd, N., Reps, T., and Touili, T.,Abstract error projection. In Proc. Static Analysis Symposium, 2007. [abstract;PDF; slides: Powerpoint;(c) Springer-Verlag]
Gopan, D. and Reps, T.,Guided static analysis. In Proc. Static Analysis Symposium, 2007. [abstract;PDF;(c) Springer-Verlag]
Lev-Ami, T., Weidenbach, C., Reps, T., and Sagiv, M.,Labelled clauses. In Proc. Conference on Automated Deduction, 2007. [abstract;PDF;(c) Springer-Verlag]
Gopan, D. and Reps, T.,Low-level library analysis and summarization. In Proc. Computer-Aided Verification, 2007. [abstract;PDF;(c) Springer-Verlag]
Amit, D., Rinetzky, N., Reps, T., Sagiv, M., and Yahav, E.,Comparison under abstraction for verifying linearizability. In Proc. Computer-Aided Verification, 2007. [abstract;PDF;(c) Springer-Verlag]
Bogudlov, I., Lev-Ami, T., Reps, T, and Sagiv, M.,Revamping TVLA: Making parametric shape analysis competitive (tool paper). In Proc. Computer-Aided Verification, 2007. [abstract;PDF;(c) Springer-Verlag]
Loginov, A., Reps, T., and Sagiv, M.,Refinement-based verification for possibly-cyclic lists. In Program Analysis and Compilation, Theory and Practice: Essays Dedicated to Reinhard Wilhelm, Springer-Verlag. [abstract;PDF;(c) Springer-Verlag]
Balakrishnan, G., Reps, T., Melski, D., and Teitelbaum, T.,WYSINWYX: What You See Is Not What You eXecute. In Verified Software: Theories, Tools, Experiments, Springer-Verlag, 2007. [abstract;PostScript;PDF;(c) Springer-Verlag]
Dor, N., Field, J., Gopan, D., Lev-Ami, T., Loginov, A., Manevich, R., Ramalingam, G., Reps, T., Rinetzky, N., Sagiv, M., Wilhelm, R., Yahav, E., and Yorsh, G.,Automatic verification of strongly dynamic software systems. In Verified Software: Theories, Tools, Experiments, Springer-Verlag, 2007. [abstract;PostScript;PDF;(c) Springer-Verlag]
Lev-Ami, T., Sagiv, M., Immerman, N., and Reps, T.,Shape analysis of uniform change. In Proc. Verification, Model Checking, and Abstract Interpretation (VMCAI), (Nice, France, Jan. 14-16, 2007). [abstract;PDF;(c) Springer-Verlag]
Lim, J., Reps, T., and Liblit, B.,Extracting output formats from executables. In Proc. IEEE Working Conference on Reverse Engineering, (Benevento, Italy, Oct. 23-27, 2006). [abstract;PDF; talk: Powerpoint]
Wang, H., Jha, S., Reps, T., Schwoon, S., and Stubblebine, S.,Reducing the dependence of SPKI/SDSI on PKI. In European Symposium on Research in Computer Security (ESORICS), 2006. [abstract;PDF;(c) Springer-Verlag]
Loginov, A., Reps, T., and Sagiv, M.,Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In Static Analysis Symposium, 2006. [abstract;PDF;(c) Springer-Verlag]
Balakrishnan, G. and Reps, T.,Recency-abstraction for heap-allocated storage. In Static Analysis Symposium, 2006. [abstract;PDF;(c) Springer-Verlag]
Lal, A. and Reps, T.,Improving pushdown system model checking. In Computer-Aided Verification 2006. [abstract;PDF;(c) Springer-Verlag]
Gopan, D. and Reps, T.,Lookahead widening. In Computer-Aided Verification 2006. [abstract;PDF;(c) Springer-Verlag]
Chaki, S., Clarke, E., Kidd, N., Reps, T., and Touili, T.,Verifying concurrent message-passing C programs with recursive calls. In Proc. TACAS, Springer-Verlag, New York, NY, 2006. [abstract;PostScript;PDF;(c) Springer-Verlag; talk: Powerpoint]
Jeannet, B., Gopan, D., and Reps, T.,A relational abstraction for functions. In Proc. 12th Int. Static Analysis Symp., 2005. [abstract;PostScript;PDF;(c) Springer-Verlag]
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. In Proc. Conf. on Automated Deduction, 2005. [abstract;PostScript;PDF;(c) Springer-Verlag; talk: Powerpoint.]
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. In Proc. Computer-Aided Verification, 2005. [abstract;PostScript;PDF;(c) Springer-Verlag]
Loginov, A., Reps, T, and Sagiv, M.,Abstraction refinement via inductive learning. 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. In Proc. Int. Conf. on Software Engineering, (St. Louis, Missouri, May 15-21, 2005). [abstract;PostScript;PDF;ACM Author-Izer Link.]
Balakrishnan, G., Gruian, R., Reps, T., and Teitelbaum, T.,CodeSurfer/x86 -- A platform for analyzing x86 executables, (tool demonstration paper). 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]
Gopan, D., Reps, T., and Sagiv, M.,A framework for 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;ACM Author-Izer Link;Powerpoint]
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;ACM Author-Izer Link.]
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;Powerpoint;(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;Powerpoint;(c) Springer-Verlag]
Reps, T., Sagiv, M., and Yorsh, G.,Symbolic implementation of the best transformer. In Proc. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2004, 252-266. [abstract;PostScript;PDF;(c) Springer-Verlag]
S. Yong and S. Horwitz,Protecting C Programs from Attacks via Invalid Pointer Dereferences. In Proceedings of the 10th ACM SIGSOFT International Symposium on Foundations of Software Engineering, (Sept 2003, Helsinki Finland), pp. 307-316. [abstract;Postscript,]
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.]
R. Komondoor and S. Horwitz,Effective, automatic procedure extraction. In Proc. 11th IEEE International Workshop on Program Comprehension, (Portland, Oregon, May 10-11, 2003). [abstract;Postscript]
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]
Yong, S. and Horwitz, S, Reducing the overhead of dynamic analysis. In Proceedings RV'02 (Second Workshop on Runtime Verification)(Copenhagen, Denmark, July 26, 2002). [postscript]
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; talk: Powerpoint.]
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]
Horwitz, S.,Tool support for improving test coverage. In Proc. of ESOP 2002: European Symp. on Programming, (Grenoble, France, April 8-12, 2002). [abstract;paper,(c) Springer-Verlag]
Kumar, S. and Horwitz, S.,Better slicing of programs with jumps and switches. In Proc. of FASE 2002: Fundamental Approaches to Softw. Eng., (Grenoble, France, April 8-12, 2002). [abstract;paper,(c) Springer-Verlag]
Komondoor, R. and Horwitz, S.,Using slicing to identify duplication in source code. In Proc. of the 8th International Symposium on Static Analysis, (Paris, France, July 16-18, 2001), [abstract;paper,(c) Springer-Verlag]
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]
Komondoor, R. and Horwitz, S.Tool Demonstration: Finding duplicated code using program dependences. In Proc. of ESOP 2001: European Symp. on Programming, (Genoa, Italy, April 2-6, 2001). [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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
Komondoor, R. and Horwitz, S., Semantics-preserving procedure extraction. In POPL '00: Proceedings of the ACM Symposium on Principles of Programming Languages, (Boston, MA, January 2000), pp. 155-169. [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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
Hasti, R. and Horwitz, S.,Using static single assignment form to improve flow-insensitive pointer analysis. In Proceedings of the ACM SIGPLAN '98 Conference on Programming Language Design and Implementation(Montreal Canada, June 16-20, 1998). [abstract;paper (postscript);paper (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;ACM Author-Izer Link.]
Shapiro, M. and Horwitz, S.,The effects of the precision of pointer analysis. In Proceedings of the 4th International Symposium on Static Analysis, (Paris, France, September 8-10, 1997),Lecture Notes in Computer Science, Vol. 1302, Pascal Van Hentenryck (ed.), Springer-Verlag, New York, NY, 1997, pp. 16-34. [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;ACM Author-Izer Link.]
Shapiro, M. and Horwitz, S.,Fast and accurate flow-insensitive points-to analysis. In Conference Record of the Twenty-Fourth ACM Symposium on Principles of Programming Languages, (Paris, France, Jan. 15-17, 1997). [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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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;PDF;ACM Author-Izer Link.]
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.**(Awarded an ACM SIGSOFT Retrospective Impact Paper Award 2011.)**[abstract;PDF;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
Ball, T. and Horwitz, S.,Slicing programs with arbitrary control flow. In Proceedings of the First International Workshop on Automated and Algorithmic Debugging, (Linkoeping, Sweden, May 1993),Lecture Notes in Computer Science, Vol. 749, Springer-Verlag, New York, NY, 1993, pp. 206-222. [paper,(c) Springer-Verlag]
Bates, S. and Horwitz, S.,Incremental program testing using program dependence graphs. In Conference Record of the Twentieth ACM Symposium on Principles of Programming Languages, (Charleston, SC, January 10-13, 1993), ACM, New York, NY, 1993, pp. 384-396. [paper]
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). [abstract;PostScript;paper;(c) Springer-Verlag]
Pfeiffer, P. and Selke, R.P.,On the adequacy of dependence-based representations for programs with heaps. In Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS '91), (Sendai, Japan, September 1991), Lecture Notes in Computer Science, Vol. 526, T. Ito and A. R. Meyer (eds.), Springer-Verlag, New York, NY, 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. [PDF.]
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. [ACM Author-Izer Link.]
Horwitz, S.,Identifying the semantic and textual differences between two versions of a program. In Proceedings of the ACM SIGPLAN 90 Conference on Programming Language Design and Implementation(White Plains, NY, June 20-22, 1990), ACM SIGPLAN Notices 25, 6 (June 1990), pp. 234-245. [PDF.]
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. [PDF.]
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. [ACM Author-Izer Link.]
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. [ACM Author-Izer Link.]
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. [PDF.]
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.**(Selected as one of the 50 most influential papers from ACM PLDI 1979-99.)**[abstract;retrospective (PS);retrospective (PDF);ACM Author-Izer Link.]
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 noninterfering 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. [ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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. [ACM Author-Izer Link.]
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.**(Awarded an ACM SIGSOFT Retrospective Impact Paper Award 2010.)**[abstract;paper;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
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. [ACM Author-Izer Link.]
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;ACM Author-Izer Link.]
[Back to the Table of Contents]

Tutorials

Material from POPL 2022 tutorial ``Program analysis via graph reachability: Past, present, and future'' (Q. Zhang and T. Reps):
- Link for slides
Material from CAV 2021 tutorial ``Introduction to Algebraic Program Analysis'' (Z. Kincaid and T. Reps):
- Part 1 (Kincaid)
- Part 2 (Kincaid)
- Part 3 (Reps)
- Part 4 (Kincaid)
Material from PLMW@PLDI21 talk ``Tips on writing a research paper'':
- Slides
- Video recording
Material from POPL 2018 tutorial ``Introduction to algebraic program analysis'' (Z. Kincaid and T. Reps):
- Part 1 (Kincaid)
- Part 2 (Kincaid)
- Part 3 (Reps)
- Part 4 (Kincaid)
Material from CAV 2010 tutorial ``'':
- Reps, T., Lim, J., Thakur, A., Balakrishnan, G., and Lal, A., There's plenty of room at the bottom: Analyzing and verifying machine code (Invited tutorial). In Proc. Computer Aided Verification, July 2010. [abstract;PDF;(c) Springer-Verlag]
- Slides: Powerpoint
Material from PLDI 2000 tutorial ``Program analysis via graph reachability'':
- 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]
- Slides: Powerpoint
Material from POPL 1993 tutorial ``Incremental computation''
- 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.) [PDF;ACM Author-Izer Link.]
- 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).) [PDF]
  [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. (Assignee: Wisconsin Alumni Research Foundation, Madison, WI.)
Alhanahnah, M., Rastogi, V., Jha, S., and Reps, T.,Computer implemented program specialization. U.S. Patent Number 12,079,607, issued September 3, 2024. (Assignee: Wisconsin Alumni Research Foundation, Madison, WI.)
[Back to the Table of Contents]

Pending Submissions

[Back to the Table of Contents]
### Ph.D. Dissertations
* Mike Vaughn, Specializing C and x86 Machine-Code Software with OS Assistance. Ph.D. dissertation, January 2024. [Link to dissertation]
* John Cyphert, Compositional, Monotone, and Non-linear Program Analysis, Ph.D. dissertation, December 2023. [Link to dissertation]
* Jordan Henkel, Learning from Code and Non-Code Artifacts. Ph.D. dissertation, Computer Sciences Department, University of Wisconsin, Madison, WI, May 2022. [PDF]
* Jason Breck, Enhancing Algebraic Program Analysis. Ph.D. dissertation and Tech. Rep. TR-1863, Computer Sciences Department, University of Wisconsin, Madison, WI, Aug. 2020. [Link to dissertation]
* David Bingham Brown, Mutation Testing: Algorithms and Applications. Ph.D. dissertation, Computer Sciences Department, University of Wisconsin, Madison, WI, Aug. 2020. [Link to dissertation]
* Tushar Sharma,Abstract Interpretation Over Bitvectors. Ph.D. dissertation and Tech. Rep. TR-1849, Computer Sciences Department, University of Wisconsin, Madison, WI, Aug. 2017. [abstract;PDF]
* Venkatesh Srinivasan,Synthesis of Machine Code: Algorithms and Applications. Ph.D. dissertation and Tech. Rep. TR-1844, Computer Sciences Department, University of Wisconsin, Madison, WI, Mar. 2017. [abstract;PDF]
For this work, Venkatesh received the UW Computer Sciences Department'sOutstanding Graduate Student Research Award for 2016-2017.
* William Harris,Secure programming via game-based synthesis. Ph.D. dissertation and Tech. Rep. TR-1814, Computer Sciences Department, University of Wisconsin, Madison, WI, Dec. 2014. (Supervised jointly with S. Jha.) [abstract;PDF] (Google Scholar,DBLP )
* Aditya Thakur,Symbolic abstraction: Algorithms and applications. Ph.D. dissertation and Tech. Rep. TR-1812, Computer Sciences Department, University of Wisconsin, Madison, WI, Aug. 2014. [abstract;PDF] (Google Scholar,Microsoft Academic Search,DBLP )
For this work, Aditya was a co-recipient of the UW Computer Sciences Department's**Outstanding Graduate Student Research Award for 2013-2014.
* Evan Driscoll,Checking format compatibility of programs using automata. Ph.D. dissertation and Tech. Rep. TR-1799, Computer Sciences Department, University of Wisconsin, Madison, WI, Aug. 2013. [abstract;dissertation]
* Junghee Lim,Transformer Specification Language: A system for generating analyzers and its applications. Ph.D. dissertation and Tech. Rep. TR-1689, Computer Sciences Department, University of Wisconsin, Madison, WI, May 2011. [abstract;PDF] (CiteseerX,Google Scholar,Microsoft Academic Search,DBLP )
For this work, Junghee received the UW Computer Sciences Department'sOutstanding Graduate Student Research Award for 2010-2011.
* Nick Kidd,Static verification of data-consistency properties. Ph.D. dissertation and Tech. Rep. TR-1665, Computer Sciences Department, University of Wisconsin, Madison, WI, August 2009. [abstract;PDF]
* Akash Lal,Interprocedural analysis and the verification of concurrent programs. Ph.D. dissertation and Tech. Rep. TR-1662, Computer Sciences Department, University of Wisconsin, Madison, WI, August 2009. [abstract;PDF]
For this work, Akash was a co-recipient of the 2009 ACM SIGPLANJohn C. Reynolds Doctoral Dissertation Award, and a co-recipient of the UW Computer Sciences Department'sOutstanding Graduate Student Research Award for 2008-2009. Akash was also named to MIT Technology Review's2011 India TR-35 list(top innovators under 35).
* Balakrishnan, G.,WYSINWYX: What You See Is Not What You eXecute. Ph.D. dissertation and Tech. Rep. TR-1603, Computer Sciences Department, University of Wisconsin, Madison, WI, August 2007. [abstract;PDF]
For this work, Gogul received the UW Computer Sciences Department'sOutstanding Graduate Student Research Award for 2007-2008**.
* Gopan, D.,Numeric program analysis techniques with applications to array analysis and library summarization. Ph.D. dissertation and Tech. Rep. TR-1602, Computer Sciences Department, University of Wisconsin, Madison, WI, August 2007. [abstract;PDF]
* Loginov, A.,Refinement-based program verification via three-valued-logic analysis. Ph.D. dissertation and Tech. Rep. TR-1574, Computer Sciences Department, University of Wisconsin, Madison, WI, August 2006. [abstract;PDF]
* Yong, S.,Runtime monitoring of C programs for security and correctness. Ph.D. dissertation, Computer Sciences Department, University of Wisconsin, Madison, WI, August 2004. [PDF]
* Komondoor, R.,Automated duplicated-code detection and procedure extraction. Ph.D. dissertation, Computer Sciences Department, University of Wisconsin, Madison, WI, August 2003. [PDF]
* 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. [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]
* Ball, T.J.,The use of control-flow and control dependence in software tools. Ph.D. dissertation and Tech. Rep. TR-1169, Computer Sciences Department, University of Wisconsin, Madison, WI, August 1993. [dissertation]
* G. Ramalingam,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. [Access via SpringerLink.]
* 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. [dissertation]
[Back to the Table of Contents]
### Magazine Articles
* Anderson, P. and Reps, T.,When good compilers go bad, or What you see is not what you execute. In Embedded Systems Design, Feb. 2010.
* Anderson, P., Reps, T., Teitelbaum, T., and Zarins, M.,Tool support for fine-grained software inspection.IEEE Software 20(4): 42-50 (2003). [abstract;paper, via IEEE Explore.]
[Back to the Table of Contents]
### Other Publications and Reports
* Yu, N., Trinh, X.D., and Reps, T.,Scalable equivalence checking and verification of shallow quantum circuits.arxiv:2504.01558, April 2025.
* Jain, A., Adiole, C., Chaudhuri, S., Reps, T., and Jermaine, C.,Coarse tuning models of code with reinforcement learning feedback.arXiv:2305.18341, May 2023.
* Henkel, J., Silva, D., Teixeira, L., d'Amorim, M., and Reps, T.W.,Shipwright: A human-in-the-loop system for Dockerfile repair. In Proc. Int. Conf. on Software Engineering (ICSE, Companion Volume), 2021, pp. 198-199.
* Henkel, J., Lahiri, S.K., Liblit, B., and Reps, T.W.,Enabling open-world specification mining via unsupervised learning.arXiv:1904.12098, Nov. 2022.
* Kashyap, V., Brown, D.B., Liblit, B., Melski, D., and Reps, T.,Source Forager: A search engine for similar source code.arXiv:1706.02769, June 2017.
* Amodio, M., Chaudhuri, S., and Reps, T.,Neural attribute machines for program generation.arXiv:1705.09231v2, May 2017.
* Henry, J., Thakur, A., Kidd, N., and Reps, T.,Dissolve: A distributed SAT solver based on Staalmarck's method. TR-1839, Computer Sciences Department, University of Wisconsin, Madison, WI, Aug. 2016. [abstract;PDF]
* Srinivasan, V. and Reps, T.,Slicing machine code. TR-1824, Computer Sciences Department, University of Wisconsin, Madison, WI, Oct. 2015. [abstract;PDF]
* Srinivasan, V. and Reps, T.,Synthesis of machine code from semantics. TR-1814, Computer Sciences Department, University of Wisconsin, Madison, WI, Feb. 2015. [abstract;PDF]
* Kroening, D., Reps, T.W., Seshia, S.A., and Thakur, A. (eds.),Decision procedures and abstract interpretation (Dagstuhl Seminar 14351), Dagstuhl Seminar Report 4, 8 (Dec. 2014) International Conference and Research Center for Computer Science (IBFI), Schloss Dagstuhl, Wadern, Germany, 2014. [URL]
* Reps, T. and Thakur, A.,Through the lens of abstraction. In Proc. of the High Confidence Software and Systems Conference (HCSS), May 2014. [PDF]
* Thakur, A., Lal, A., Lim, J., and Reps, T.,PostHat and all that: Attaining most-precise inductive invariants. TR-1790, Computer Sciences Department, University of Wisconsin, Madison, WI, April 2013. [abstract;PDF]
* Sharma, T., Thakur, A., and Reps, T.,An abstract domain for bit-vector inequalities. TR-1789, Computer Sciences Department, University of Wisconsin, Madison, WI, April 2013. [abstract;PDF]
* Srinivasan, V.K. and Reps, T.,Software-architecture recovery from machine code. TR-1781, Computer Sciences Department, University of Wisconsin, Madison, WI, March 2013. [abstract;PDF]
* King, A.M., Mycroft, A., Reps, T.W., and Simon, A. (eds.), Analysis of executables: Benefits and challenges (Dagstuhl Seminar 12051) Dagstuhl Seminar Report 2, 1 (May 2012) International Conference and Research Center for Computer Science (IBFI), Schloss Dagstuhl, Wadern, Germany, 2012. [URL]
* Harris, W.R., Farley, B., Jha, S., and Reps, T.,Programming for a capability system via safety games, TR-1705, Computer Sciences Department, University of Wisconsin, Madison, WI, March 2012. [abstract;PDF]
* Prabhu, P., Reps, T., Lal, A., and Kidd, N.Verifying concurrent programs via bounded context-switching and induction. TR-1701, Computer Sciences Department, University of Wisconsin, Madison, WI, November 2011. [abstract;PDF]
* Driscoll, E., Thakur, A., Burton, A., and Reps, T.,WALi: Nested-word automata. TR-1675r, Computer Sciences Department, University of Wisconsin, Madison, WI, July 2010; revised Sept. 2011. [abstract;PDF]
* Lim, J. and Reps, T.,BCE: Extracting botnet commands from bot executables. TR-1668, Computer Sciences Department, University of Wisconsin, Madison, WI, February 2010. [abstract;PDF]
* Lal, A., Lim, J., and Reps, T.,McDash: Refinement-based property verification for machine code. TR-1659, Computer Sciences Department, University of Wisconsin, Madison, WI, June 2009. [abstract;PDF]
* Lev-Ami, T., Sagiv, M., Reps, T., and Gulwani, S.,Backward analysis for inferring quantified preconditions. Tech. Rep. TR-2007-12-01, Tel Aviv University, Dec. 2007. [PDF]
* Kidd, N., Moore, K., Wood, D., and Reps, T.,Towards the analysis of transactional software. TR-1624, Computer Sciences Department, University of Wisconsin, Madison, WI, October 2007. [abstract;PDF]
* Kidd, N., Reps, T., Dolby, J., and Vaziri, M.,Static detection of atomic-set serializability violations. TR-1623, Computer Sciences Department, University of Wisconsin, Madison, WI, October 2007. [abstract;PDF]
* Kidd, N., Lal, A., and Reps, T.,Advanced querying for property checking. TR-1621, Computer Sciences Department, University of Wisconsin, Madison, WI, October 2007. [abstract;PDF]
* Lal, A., Touili, T., Kidd, N., and Reps, T.Weighted pushdown systems and weighted transducers. TR-1581, Computer Sciences Department, University of Wisconsin, Madison, WI, Oct. 2006. [abstract;PDF]
* 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++. In Proc. Workshop on the Evaluation of Software Defect Detection Tools, June 2005.
* Yahav, E., Pnueli, A., Reps, T., and Sagiv, M.,Automatic verification of temporal heap properties. April 2004.
* 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. BL011350-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
* 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. [PDF,PostScript]
* 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.) [PDF;ACM Author-Izer Link.]
* 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).) [PDF]
* Ball, T., and Horwitz. S., Slicing Programs with Arbitrary Control Flow. TR-92-1128, Computer Sciences Department, University of Wisconsin-Madison, December 1992.tr-92-1128.ps.
* 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. [ACM Author-Izer Link.]
* Ball, T., and Horwitz. S., Constructing Control Flow from Control Dependence. TR-92-1091, Computer Sciences Department, University of Wisconsin-Madison, June 1992.tr-92-1091.ps.
* 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]
* Yang, W., Horwitz, S. and Reps, T.Detecting program components with equivalent behaviors. TR-840, Computer Sciences Department, University of Wisconsin-Madison, April 1989. tr840.ps
* 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 Table of Contents]

Software

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., Rosay, G., and Horwitz, S., The Wisconsin Program-Slicing Tool. Release 1.0, August 1997.
Kidd, N., Reps, T., Melski, D., and Lal, A., WPDS++: A C++ Library for Weighted Pushdown Systems, 2004. (Download software from here.)
Kidd, N., Lal, A., and Reps, T., WALi: The Weighted Automaton Library, December 2007. (GitHub site.)
Driscoll, E., Thakur, A., and Reps, T., OpenNWA: A Nested-Word Automaton Library, March 2012. (GitHub site.)
Raghavan, K.V., Software for detecting clones in C code, Feb. 2014. (Download software from here. You will also need a copy ofCodeSurfer/C.)
[Back to the Table of Contents]

Wisconsin Program-Slicing Project's Home Page (original) (raw)

Table of Contents

Disclaimer

Research Summary

Recent Items of Note

Recent Publications

Miscellaneous

Personnel

Faculty

Former Students, Post-Doctoral Associates, Staff, and Visitors

Categorized Index to Project Publications

Program Slicing, Differencing, Merging, etc.

Overview

The Wisconsin Program-Slicing Tool

CodeSurfer System

Slicing

Chopping

Differencing

Merging

Algebra of slices (and applications to program merging)

Semantics and slicing

Other applications of slicing

Implemented integration system (for a small Pascal subset)

Miscellaneous

Ph.D. Dissertations

Interprocedural Dataflow Analysis

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

Exhaustive and Demand IDFA via graph reachability

IDFA using more than graph reachability

PTIME completeness of IDFA

Alias Analysis, Pointer Analysis, and Shape Analysis

Ph.D. Dissertations

Analysis of Multi-Threaded Programs

Ph.D. Dissertations

Symbolic Abstraction and Decision Procedures

Ph.D. Dissertations

Other Program-Analysis Problems

Ph.D. Dissertations

Path Problems

Context-Free-Language Reachability

Other Path Problems

Ph.D. Dissertations

Model Checking

Software

Ph.D. Dissertations

Computer Security

Ph.D. Dissertations

Quantum Computing

Code Instrumentation

Ph.D. Dissertations

Computational Differentiation and Computational Divided Differencing

Clone Detection

Software

Ph.D. Dissertations

Miscellaneous

Project Bibliography

Books

Journal Publications

Invited Papers

Book Chapters

Reprinted in Collections

Edited Books

Conference and Refereed Workshop Publications

Tutorials

Patents

Pending Submissions

Software