| 2024 | CAV | The SemGuS Toolkit. | Keith J. C. Johnson, Andrew Reynolds, Thomas W. Reps, Loris D'Antoni |
| 2024 | SAS | Synthesizing Abstract Transformers for Reduced-Product Domains. | Pankaj Kumar Kalita, Thomas W. Reps, Subhajit Roy |
| 2023 | CAV | Symbolic Quantum Simulation with Quasimodo. | Meghana Sistla, Swarat Chaudhuri, Thomas W. Reps |
| 2023 | FMCAD | Modular System Synthesis. | Kanghee Park, Keith J. C. Johnson, Loris D'Antoni, Thomas W. Reps |
| 2021 | CAV | Programmable Program Synthesis. | Loris D'Antoni, Qinheping Hu, Jinwoo Kim, Thomas W. Reps |
| 2021 | CAV | Synthesis with Asymptotic Resource Bounds. | Qinheping Hu, John Cyphert, Loris D'Antoni, Thomas W. Reps |
| 2021 | CAV | Algebraic Program Analysis. | Zachary Kincaid, Thomas W. Reps, John Cyphert |
| 2021 | ICSE | Shipwright: A Human-in-the-Loop System for Dockerfile Repair. | Jordan Henkel, Denini Silva, Leopoldo Teixeira, Marcelo d'Amorim, Thomas W. Reps |
| 2021 | ICSE | Shipwright: A Human-in-the-Loop System for Dockerfile Repair. | Jordan Henkel, Denini Silva, Leopoldo Teixeira, Marcelo d'Amorim, Thomas W. Reps |
| 2021 | PLDI | Central moment analysis for cost accumulators in probabilistic programs. | Di Wang, Jan Hoffmann, Thomas W. Reps |
| 2021 | PLDI | Sound probabilistic inference via guide types. | Di Wang, Jan Hoffmann, Thomas W. Reps |
| 2020 | ICSE | Learning from, understanding, and supporting DevOps artifacts for docker. | Jordan Henkel, Christian Bird, Shuvendu K. Lahiri, Thomas W. Reps |
| 2020 | MSR | A Dataset of Dockerfiles. | Jordan Henkel, Christian Bird, Shuvendu K. Lahiri, Thomas W. Reps |
| 2020 | PLDI | Templates and recurrences: better together. | Jason Breck, John Cyphert, Zachary Kincaid, Thomas W. Reps |
| 2020 | PLDI | Exact and approximate methods for proving unrealizability of syntax-guided synthesis problems. | Qinheping Hu, John Cyphert, Loris D'Antoni, Thomas W. Reps |
| 2020 | PLDI | Fast graph simplification for interleaved Dyck-reachability. | Yuanbo Li, Qirun Zhang, Thomas W. Reps |
| 2019 | CAV | Proving Unrealizability for Syntax-Guided Synthesis. | Qinheping Hu, Jason Breck, John Cyphert, Loris D'Antoni, Thomas W. Reps |
| 2018 | PLDI | PMAF: an algebraic framework for static analysis of probabilistic programs. | Di Wang, Jan Hoffmann, Thomas W. Reps |
| 2017 | CAV | Automated Resource Analysis with Coq Proof Objects. | Quentin Carbonneaux, Jan Hoffmann, Thomas W. Reps, Zhong Shao |
| 2017 | PLDI | Compositional recurrence analysis revisited. | Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, Thomas W. Reps |
| 2017 | POPL | Component-based synthesis for complex APIs. | Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, Thomas W. Reps |
| 2017 | SAS | A New Abstraction Framework for Affine Transformers. | Tushar Sharma, Thomas W. Reps |
| 2017 | VMCAI | Sound Bit-Precise Numerical Domains. | Tushar Sharma, Thomas W. Reps |
| 2016 | ESOP | An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs. | Antoine Min, Jason Breck, Thomas W. Reps |
| 2016 | OOPSLA | An improved algorithm for slicing machine code. | Venkatesh Srinivasan, Thomas W. Reps |
| 2016 | OOPSLA | Speeding up machine-code synthesis. | Venkatesh Srinivasan, Tushar Sharma, Thomas W. Reps |
| 2016 | POPL | Newtonian program analysis via tensor product. | Thomas W. Reps, Emma Turetsky, Prathmesh Prabhu |
| 2016 | VMCAI | Automating Abstract Interpretation. | Thomas W. Reps, Aditya V. Thakur |
| 2015 | OOPSLA | Recovering execution data from incomplete observations. | Peter Ohmann, David Bingham Brown, Ben Liblit, Thomas W. Reps |
| 2015 | OOPSLA | Partial evaluation of machine code. | Venkatesh Srinivasan, Thomas W. Reps |
| 2015 | PLDI | Synthesis of machine code from semantics. | Venkatesh Srinivasan, Thomas W. Reps |
| 2014 | CAV | Property-Directed Shape Analysis. | Shachar Itzhaky, Nikolaj S. Bjrner, Thomas W. Reps, Mooly Sagiv, Aditya V. Thakur |
| 2014 | CC | Recovery of Class Hierarchies and Composition Relationships from Machine Code. | Venkatesh Srinivasan, Thomas W. Reps |
| 2014 | PLDI | Specialization slicing. | Min Aung, Susan Horwitz, Richard Joiner, Thomas W. Reps |
| 2013 | FMCAD | Secure programs via game-based synthesis. | Somesh Jha, Thomas W. Reps, William R. Harris |
| 2013 | SP | Declarative, Temporal, and Practical Programming with Capabilities. | William R. Harris, Somesh Jha, Thomas W. Reps, Jonathan Anderson, Robert N. M. Watson |
| 2012 | CAV | OpenNWA: A Nested-Word Automaton Library. | Evan Driscoll, Aditya V. Thakur, Thomas W. Reps |
| 2012 | CAV | Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement. | Matthew Fredrikson, Richard Joiner, Somesh Jha, Thomas W. Reps, Phillip A. Porras, Hassen Sadi, Vinod Yegneswaran |
| 2012 | CAV | Secure Programming via Visibly Pushdown Safety Games. | William R. Harris, Somesh Jha, Thomas W. Reps |
| 2012 | CAV | A Method for Symbolic Computation of Abstract Operations. | Aditya V. Thakur, Thomas W. Reps |
| 2012 | SAS | Bilateral Algorithms for Symbolic Abstraction. | Aditya V. Thakur, Matt Elder, Thomas W. Reps |
| 2012 | SAS | A Generalization of Stlmarck's Method. | Aditya V. Thakur, Thomas W. Reps |
| 2011 | ASPLOS | ConSeq: detecting concurrency bugs through sequential errors. | Wei Zhang, Junghee Lim, Ramya Olichandran, Joel Scherpelz, Guoliang Jin, Shan Lu, Thomas W. Reps |
| 2011 | SAS | Abstract Domains of Affine Relations. | Matt Elder, Junghee Lim, Tushar Sharma, Tycho Andersen, Thomas W. Reps |
| 2010 | CAV | There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code. | Thomas W. Reps, Junghee Lim, Aditya V. Thakur, Gogul Balakrishnan, Akash Lal |
| 2010 | CAV | Directed Proof Generation for Machine Code. | Aditya V. Thakur, Junghee Lim, Akash Lal, Amanda Burton, Evan Driscoll, Matt Elder, Tycho Andersen, Thomas W. Reps |
| 2010 | CCS | DIFC programs by automatic instrumentation. | William R. Harris, Somesh Jha, Thomas W. Reps |
| 2010 | SAS | Statically Inferring Complex Heap, Array, and Numeric Invariants. | Bill McCloskey, Thomas W. Reps, Mooly Sagiv |
| 2009 | FM | Verifying Information Flow Control over Unbounded Processes. | William R. Harris, Nicholas Kidd, Sagar Chaki, Somesh Jha, Thomas W. Reps |
| 2009 | VMCAI | Finding Concurrency-Related Bugs Using Random Isolation. | Nicholas Kidd, Thomas W. Reps, Julian Dolby, Mandana Vaziri |
| 2008 | CAV | Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. | Akash Lal, Thomas W. Reps |
| 2008 | CC | A System for Generating Static Analyzers for Machine Instructions. | Junghee Lim, Thomas W. Reps |
| 2008 | CC | Improved Memory-Access Analysis for x86 Executables. | Thomas W. Reps, Gogul Balakrishnan |
| 2008 | SAS | Language Strength Reduction. | Nicholas Kidd, Akash Lal, Thomas W. Reps |
| 2008 | SAS | Solving Multiple Dataflow Queries Using WPDSs. | Akash Lal, Thomas W. Reps |
| 2008 | TACAS | Analyzing Stripped Device-Driver Executables. | Gogul Balakrishnan, Thomas W. Reps |
| 2008 | TACAS | Interprocedural Analysis of Concurrent Programs Under a Context Bound. | Akash Lal, Tayssir Touili, Nicholas Kidd, Thomas W. Reps |
| 2007 | CADE | Labelled Clauses. | Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv |
| 2007 | CAV | Comparison Under Abstraction for Verifying Linearizability. | Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, Eran Yahav |
| 2007 | CAV | Revamping TVLA: Making Parametric Shape Analysis Competitive. | Igor Bogudlov, Tal Lev-Ami, Thomas W. Reps, Mooly Sagiv |
| 2007 | CAV | Low-Level Library Analysis and Summarization. | Denis Gopan, Thomas W. Reps |
| 2007 | SAS | Guided Static Analysis. | Denis Gopan, Thomas W. Reps |
| 2007 | SAS | Abstract Error Projection. | Akash Lal, Nicholas Kidd, Thomas W. Reps, Tayssir Touili |
| 2007 | VMCAI | DIVINE: DIscovering Variables IN Executables. | Gogul Balakrishnan, Thomas W. Reps |
| 2007 | VMCAI | Constructing Specialized Shape Analyses for Uniform Change. | Tal Lev-Ami, Mooly Sagiv, Neil Immerman, Thomas W. Reps |
| 2006 | CAV | Lookahead Widening. | Denis Gopan, Thomas W. Reps |
| 2006 | CAV | Improving Pushdown System Model Checking. | Akash Lal, Thomas W. Reps |
| 2006 | ESORICS | Reducing the Dependence of SPKI/SDSI on PKI. | Hao Wang, Somesh Jha, Thomas W. Reps, Stefan Schwoon, Stuart G. Stubblebine |
| 2006 | PEPM | Intermediate-representation recovery from low-level code. | Thomas W. Reps, Gogul Balakrishnan, Junghee Lim |
| 2006 | SAS | Recency-Abstraction for Heap-Allocated Storage. | Gogul Balakrishnan, Thomas W. Reps |
| 2006 | SAS | Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm. | Alexey Loginov, Thomas W. Reps, Mooly Sagiv |
| 2006 | TACAS | Verifying Concurrent Message-Passing C Programs with Recursive Calls. | Sagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili |
| 2006 | TACAS | Weighted Pushdown Systems and Trust-Management Systems. | Somesh Jha, Stefan Schwoon, Hao Wang, Thomas W. Reps |
| 2005 | APLAS | A Next-Generation Platform for Analyzing Executables. | Thomas W. Reps, Gogul Balakrishnan, Junghee Lim, Tim Teitelbaum |
| 2005 | CADE | Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures. | Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, Siddharth Srivastava, Greta Yorsh |
| 2005 | CAV | Model Checking x86 Executables with CodeSurfer/x86 and WPDS++. | Gogul Balakrishnan, Thomas W. Reps, Nicholas Kidd, Akash Lal, Junghee Lim, David Melski, Radu Gruian, Suan Hsi Yong, Chi-Hua Chen, Tim Teitelbaum |
| 2005 | CAV | Extended Weighted Pushdown Systems. | Akash Lal, Thomas W. Reps, Gogul Balakrishnan |
| 2005 | CAV | Abstraction Refinement via Inductive Learning. | Alexey Loginov, Thomas W. Reps, Shmuel Sagiv |
| 2005 | CC | CodeSurfer/x86-A Platform for Analyzing x86 Executables. | Gogul Balakrishnan, Radu Gruian, Thomas W. Reps, Tim Teitelbaum |
| 2005 | ICSE | Automatic discovery of API-level exploits. | Vinod Ganapathy, Sanjit A. Seshia, Somesh Jha, Thomas W. Reps, Randal E. Bryant |
| 2005 | POPL | A framework for numeric analysis of array operations. | Denis Gopan, Thomas W. Reps, Shmuel Sagiv |
| 2005 | POPL | A semantics for procedure local heaps and its abstractions. | Noam Rinetzky, Jrg Bauer, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2005 | SAS | A Relational Abstraction for Functions. | Bertrand Jeannet, Denis Gopan, Thomas W. Reps |
| 2004 | CAV | Verification via Structure Simulation. | Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh |
| 2004 | CAV | Static Program Analysis via 3-Valued Logic. | Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2004 | CC | Analyzing Memory Accesses in x86 Executables. | Gogul Balakrishnan, Thomas W. Reps |
| 2004 | CSL | The Boundary Between Decidability and Undecidability for Transitive-Closure Logics. | Neil Immerman, Alexander Moshe Rabinovich, Thomas W. Reps, Shmuel Sagiv, Greta Yorsh |
| 2004 | SAS | A Relational Approach to Interprocedural Shape Analysis. | Bertrand Jeannet, Alexey Loginov, Thomas W. Reps, Shmuel Sagiv |
| 2004 | TACAS | Numeric Domains with Summarized Dimensions. | Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv |
| 2004 | TACAS | Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. | Greta Yorsh, Thomas W. Reps, Shmuel Sagiv |
| 2004 | VMCAI | Symbolic Implementation of the Best Transformer. | Thomas W. Reps, Shmuel Sagiv, Greta Yorsh |
| 2003 | CC | The Interprocedural Express-Lane Transformation. | David Melski, Thomas W. Reps |
| 2003 | ESOP | Finite Differencing of Logical Formulas for Static Analysis. | Thomas W. Reps, Shmuel Sagiv, Alexey Loginov |
| 2003 | ESOP | Verifying Temporal Heap Properties Specified via Evolution Logic. | Eran Yahav, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2003 | SAS | Weighted Pushdown Systems and Their Application to Interprocedural Dataflow Analysis. | Thomas W. Reps, Stefan Schwoon, Somesh Jha |
| 2002 | LICS | Semantic Minimization of 3-Valued Propositional Formulae. | Thomas W. Reps, Alexey Loginov, Shmuel Sagiv |
| 2002 | SAS | Static Program Analysis via 3-Valued Logic. | Thomas W. Reps |
| 2001 | ESOP | Typestate Checking of Machine Code. | Zhichen Xu, Thomas W. Reps, Barton P. Miller |
| 2001 | FASE | Debugging via Run-Time Type Checking. | Alexey Loginov, Suan Hsi Yong, Susan Horwitz, Thomas W. Reps |
| 2001 | ICALP | Model Checking of Unrestricted Hierarchical State Machines. | Michael Benedikt, Patrice Godefroid, Thomas W. Reps |
| 2000 | CC | Shape Analysis. | Reinhard Wilhelm, Shmuel Sagiv, Thomas W. Reps |
| 2000 | ISSTA | Putting static analysis to work for verification: A case study. | Tal Lev-Ami, Thomas W. Reps, Shmuel Sagiv, Reinhard Wilhelm |
| 2000 | PLDI | Safety checking of machine code. | Zhichen Xu, Barton P. Miller, Thomas W. Reps |
| 1999 | CC | Interprocedural Path Profiling. | David Melski, Thomas W. Reps |
| 1999 | ESOP | A Decidable Logic for Describing Linked Data Structures. | Michael Benedikt, Thomas W. Reps, Shmuel Sagiv |
| 1999 | PLDI | Pointer Analysis for Programs with Structures and Casting. | Suan Hsi Yong, Susan Horwitz, Thomas W. Reps |
| 1999 | POPL | Parametric Shape Analysis via 3-Valued Logic. | Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm |
| 1997 | GI | The Use of Program Profiling for Software Testing. | Thomas W. Reps |
| 1997 | PEPM | Interconveritibility of Set Constraints and Context-Free Language Reachability. | David Melski, Thomas W. Reps |
| 1996 | POPL | Solving Shape-Analysis Problems in Languages with Destructive Updating. | Shmuel Sagiv, Thomas W. Reps, Reinhard Wilhelm |
| 1995 | PEPM | Semantic Foundations of Binding Time Analysis for Imperative Programs. | Manuvir Das, Thomas W. Reps, Pascal Van Hentenryck |
| 1995 | PEPM | Shape Analysis as a Generalized Path Problem. | Thomas W. Reps |
| 1995 | POPL | Precise Interprocedural Dataflow Analysis via Graph Reachability. | Thomas W. Reps, Susan Horwitz, Shmuel Sagiv |
| 1994 | CC | Solving Demand Versions of Interprocedural Analysis Problems. | Thomas W. Reps |
| 1994 | POPL | An Incremental Algorithm for Maintaining the Dominator Tree of a Reducible Flowgraph. | G. Ramalingam, Thomas W. Reps |
| 1993 | POPL | A Categorized Bibliography on Incremental Computation. | G. Ramalingam, Thomas W. Reps |
| 1993 | SPAA | Scan Grammars: Parallel Attribute Evaluation via Data-Parallelism. | Thomas W. Reps |
| 1992 | ICSE | The Use of Program Dependence Graphs in Software Engineering. | Susan Horwitz, Thomas W. Reps |
| 1990 | ESOP | Algebraic Properties of Program Integration. | Thomas W. Reps |
| 1989 | PLDI | Dependence Analysis for Pointer Variables. | Susan Horwitz, Phil Pfeiffer, Thomas W. Reps |
| 1988 | ESOP | Semantics-Based Program Integration. | Thomas W. Reps, Susan Horwitz |
| 1988 | PLDI | Interprocedural Slicing Using Dependence Graphs. | Susan Horwitz, Thomas W. Reps, David W. Binkley |
| 1988 | PLDI | Interprocedural slicing using dependence graphs (with retrospective) | Susan Horwitz, Thomas W. Reps, David W. Binkley |
| 1988 | POPL | Integrating Non-Interfering Versions of Programs. | Susan Horwitz, Jan F. Prins, Thomas W. Reps |
| 1988 | POPL | On the Adequacy of Program Dependence Graphs for Representing Programs. | Susan Horwitz, Jan F. Prins, Thomas W. Reps |
| 1986 | POPL | Remote Attribute Updating for Language-Based Editors. | Thomas W. Reps, Carla Marceau, Tim Teitelbaum |
| 1984 | POPL | Interactive Proof Checking. | Thomas W. Reps, Bowen Alpern |
| 1982 | POPL | Optimal-Time Incremental Semantic Analysis for Syntax-Directed Editors. | Thomas W. Reps |
| 1981 | POPL | Incremental Evaluation for Attribute Grammars with Application to Syntax-Directed Editors. | Alan J. Demers, Thomas W. Reps, Tim Teitelbaum |