BibSLEIGH — Thomas_W

Travelled to:

1 × Australia
1 × Canada
1 × China
1 × Estonia
1 × Greece
1 × Korea
1 × Switzerland
2 × Austria
3 × Denmark
3 × Germany
3 × Hungary
3 × Poland
30 × USA
4 × Spain
4 × The Netherlands
6 × Italy
6 × United Kingdom
7 × France

Collaborated with:

S.Sagiv S.Horwitz G.Balakrishnan ∅ A.Lal V.Srinivasan D.Gopan A.V.Thakur R.Wilhelm J.Lim A.Loginov M.Sagiv S.Jha D.Melski N.Kidd J.Breck G.Ramalingam G.Yorsh M.Siff T.Lev-Ami T.Teitelbaum Z.Kincaid J.Cyphert B.Liblit N.Immerman E.Driscoll G.Rosay T.Touili S.Chandra S.H.Yong Z.Xu B.P.Miller M.Benedikt D.Binkley J.Prins M.Elder R.Joiner S.Schwoon B.Jeannet M.Das J.H.0002 W.R.Harris T.Sharma B.Alpern W.Yang A.Burton E.Yahav T.Ball V.Ganapathy S.Chaki N.Rinetzky A.M.Rabinovich R.Gruian B.McCloskey P.Godefroid P.V.Hentenryck P.Pfeiffer C.Marceau A.J.Demers A.Miné Ara Vartanian Emma Turetsky Prathmesh Prabhu D.Wang T.Andersen M.Aung J.Dolby M.Vaziri C.Weidenbach I.Bogudlov H.Wang J.R.Larus D.B.Brown M.Vaughn J.Henkel S.K.Lahiri Q.Carbonneaux Z.Shao Ashkan Forouhi Boroujeni S.Itzhaky N.Bjørner M.Dhawan D.Amit E.M.Clarke S.A.Seshia R.E.Bryant J.Bauer F.DiMaio N.Dor K.Kunchithapadam Q.Hu L.D'Antoni Y.Feng R.Martins Yuepeng Wang 0001 I.Dillig S.Srivastava M.Fredrikson P.A.Porras H.Saïdi V.Yegneswaran W.Zhang R.Olichandran J.Scherpelz G.Jin S.Lu C.Chen

Talks about:

analysi (36) program (24) code (14) interprocedur (13) abstract (12) machin (12) static (9) shape (9) check (9) logic (8)

Person: Thomas W. Reps

DBLP: Reps:Thomas_W=

Facilitated 1 volumes:

Contributed to:

2015

2014

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1997

1996

1995

1994

1993

1992

1990

1991

1989

1988

1986

1984

1982

1981

2017

2018

1989

1991

1995

1996

2016

2017

2019

2016

2017

2016

2017

2018

2019

Wrote 125 papers:

OOPSLA-2015-SrinivasanR #partial evaluation: Partial evaluation of machine code (VS, TWR), pp. 860–879.
PLDI-2015-SrinivasanR #semantics #synthesis: Synthesis of machine code from semantics (VS, TWR), pp. 596–607.
CAV-2014-ItzhakyBRST #analysis: Property-Directed Shape Analysis (SI, NB, TWR, MS, AVT), pp. 35–51.
CC-2014-SrinivasanR #composition: Recovery of Class Hierarchies and Composition Relationships from Machine Code (VS, TWR), pp. 61–84.
FSE-2014-JoinerRJDG #performance #policy #weaving: Efficient runtime-enforcement techniques for policy weaving (RJ, TWR, SJ, MD, VG), pp. 224–234.
PLDI-2014-AungHJR #slicing: Specialization slicing (MA, SH, RJ, TWR), p. 19.
CAV-2012-DriscollTR #automaton #library #named: OpenNWA: A Nested-Word Automaton Library (ED, AVT, TWR), pp. 665–671.
CAV-2012-FredriksonJJRPSY #abstraction #performance #policy #refinement #runtime #using: Efficient Runtime Policy Enforcement Using Counterexample-Guided Abstraction Refinement (MF, RJ, SJ, TWR, PAP, HS, VY), pp. 548–563.
CAV-2012-HarrisJR #automaton #game studies #programming #safety: Secure Programming via Visibly Pushdown Safety Games (WRH, SJ, TWR), pp. 581–598.
CAV-2012-ThakurR #symbolic computation: A Method for Symbolic Computation of Abstract Operations (AVT, TWR), pp. 174–192.
SAS-2012-ThakurER #abstraction #algorithm: Bilateral Algorithms for Symbolic Abstraction (AVT, ME, TWR), pp. 111–128.
SAS-2012-ThakurR: A Generalization of Stålmarck’s Method (AVT, TWR), pp. 334–351.
ASPLOS-2011-ZhangLOSJLR #concurrent #debugging #detection #fault #named: ConSeq: detecting concurrency bugs through sequential errors (WZ, JL, RO, JS, GJ, SL, TWR), pp. 251–264.
ESEC-FSE-2011-DriscollBR #consistency: Checking conformance of a producer and a consumer (ED, AB, TWR), pp. 113–123.
SAS-2011-ElderLSAR #abstract domain: Abstract Domains of Affine Relations (ME, JL, TS, TA, TWR), pp. 198–215.
CAV-2010-RepsLTBL #verification: There’s Plenty of Room at the Bottom: Analyzing and Verifying Machine Code (TWR, JL, AVT, GB, AL), pp. 41–56.
CAV-2010-ThakurLLBDEAR #generative #proving: Directed Proof Generation for Machine Code (AVT, JL, AL, AB, ED, ME, TA, TWR), pp. 288–305.
SAS-2010-McCloskeyRS #array #invariant: Statically Inferring Complex Heap, Array, and Numeric Invariants (BM, TWR, MS), pp. 71–99.
FM-2009-HarrisKCJR #bound #data flow #process #verification: Verifying Information Flow Control over Unbounded Processes (WRH, NK, SC, SJ, TWR), pp. 773–789.
VMCAI-2009-KiddRDV #debugging #random #using: Finding Concurrency-Related Bugs Using Random Isolation (NK, TWR, JD, MV), pp. 198–213.
CAV-2008-LalR #analysis #bound #concurrent: Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis (AL, TWR), pp. 37–51.
CC-2008-LimR #bytecode #generative: A System for Generating Static Analyzers for Machine Instructions (JL, TWR), pp. 36–52.
CC-2008-RepsB #analysis #bytecode: Improved Memory-Access Analysis for x86 Executables (TWR, GB), pp. 16–35.
SAS-2008-KiddLR #reduction: Language Strength Reduction (NK, AL, TWR), pp. 283–298.
SAS-2008-LalR #data flow #multi #query #using: Solving Multiple Dataflow Queries Using WPDSs (AL, TWR), pp. 93–109.
TACAS-2008-BalakrishnanR #bytecode: Analyzing Stripped Device-Driver Executables (GB, TWR), pp. 124–140.
TACAS-2008-LalTKR #analysis #bound #concurrent #interprocedural #source code: Interprocedural Analysis of Concurrent Programs Under a Context Bound (AL, TT, NK, TWR), pp. 282–298.
CADE-2007-Lev-AmiWRS: Labelled Clauses (TLA, CW, TWR, MS), pp. 311–327.
CAV-2007-AmitRRSY #abstraction #comparison #verification: Comparison Under Abstraction for Verifying Linearizability (DA, NR, TWR, MS, EY), pp. 477–490.
CAV-2007-BogudlovLRS #analysis #parametricity: Revamping TVLA: Making Parametric Shape Analysis Competitive (IB, TLA, TWR, MS), pp. 221–225.
CAV-2007-GopanR #analysis #library #low level #summary: Low-Level Library Analysis and Summarization (DG, TWR), pp. 68–81.
SAS-2007-GopanR #static analysis: Guided Static Analysis (DG, TWR), pp. 349–365.
SAS-2007-LalKRT #fault: Abstract Error Projection (AL, NK, TWR, TT), pp. 200–217.
VMCAI-2007-BalakrishnanR #bytecode #named: DIVINE: DIscovering Variables IN Executables (GB, TWR), pp. 1–28.
VMCAI-2007-Lev-AmiSIR #analysis: Constructing Specialized Shape Analyses for Uniform Change (TLA, MS, NI, TWR), pp. 215–233.
CAV-2006-GopanR #lookahead: Lookahead Widening (DG, TWR), pp. 452–466.
CAV-2006-LalR #automaton #model checking: Improving Pushdown System Model Checking (AL, TWR), pp. 343–357.
PEPM-2006-RepsBL #low level: Intermediate-representation recovery from low-level code (TWR, GB, JL), pp. 100–111.
SAS-2006-BalakrishnanR: Recency-Abstraction for Heap-Allocated Storage (GB, TWR), pp. 221–239.
SAS-2006-LoginovRS #algorithm #automation #verification: Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm (AL, TWR, MS), pp. 261–279.
TACAS-2006-ChakiCKRT #c #concurrent #message passing #recursion #source code #verification: Verifying Concurrent Message-Passing C Programs with Recursive Calls (SC, EMC, NK, TWR, TT), pp. 334–349.
TACAS-2006-JhaSWR #automaton #trust: Weighted Pushdown Systems and Trust-Management Systems (SJ, SS, HW, TWR), pp. 1–26.
WCRE-2006-LimRL #bytecode: Extracting Output Formats from Executables (JL, TWR, BL), pp. 167–178.
CADE-2005-Lev-AmiIRSSY #data type #first-order #linked data #logic #open data #reachability #simulation #using #verification: Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures (TLA, NI, TWR, SS, SS, GY), pp. 99–115.
CAV-2005-BalakrishnanRKLLMGYCT #bytecode #model checking: Model Checking x86 Executables with CodeSurfer/x86 and WPDS++ (GB, TWR, NK, AL, JL, DM, RG, SHY, CHC, TT), pp. 158–163.
CAV-2005-LalRB #automaton: Extended Weighted Pushdown Systems (AL, TWR, GB), pp. 434–448.
CAV-2005-LoginovRS #abstraction #induction #learning #refinement: Abstraction Refinement via Inductive Learning (AL, TWR, SS), pp. 519–533.
CC-2005-BalakrishnanGRT #bytecode #framework #named #platform: CodeSurfer/x86 — A Platform for Analyzing x86 Executables (GB, RG, TWR, TT), pp. 250–254.
ICSE-2005-GanapathySJRB #automation: Automatic discovery of API-level exploits (VG, SAS, SJ, TWR, REB), pp. 312–321.
POPL-2005-GopanRS #analysis #array #framework: A framework for numeric analysis of array operations (DG, TWR, SS), pp. 338–350.
POPL-2005-RinetzkyBRSW #abstraction #semantics: A semantics for procedure local heaps and its abstractions (NR, JB, TWR, SS, RW), pp. 296–309.
SAS-2005-JeannetGR #abstraction #relational: A Relational Abstraction for Functions (BJ, DG, TWR), pp. 186–202.
CAV-2004-ImmermanRRSY #simulation #verification: Verification via Structure Simulation (NI, AMR, TWR, SS, GY), pp. 281–294.
CAV-2004-RepsSW #logic #program analysis: Static Program Analysis via 3-Valued Logic (TWR, SS, RW), pp. 15–30.
CC-2004-BalakrishnanR #bytecode #memory management: Analyzing Memory Accesses in x86 Executables (GB, TWR), pp. 5–23.
CSL-2004-ImmermanRRSY #bound #decidability #logic #transitive: The Boundary Between Decidability and Undecidability for Transitive-Closure Logics (NI, AMR, TWR, SS, GY), pp. 160–174.
SAS-2004-JeannetLRS #analysis #approach #interprocedural #relational: A Relational Approach to Interprocedural Shape Analysis (BJ, AL, TWR, SS), pp. 246–264.
TACAS-2004-GopanDDRS: Numeric Domains with Summarized Dimensions (DG, FD, ND, TWR, SS), pp. 512–529.
TACAS-2004-YorshRS #analysis: Symbolically Computing Most-Precise Abstract Operations for Shape Analysis (GY, TWR, SS), pp. 530–545.
VMCAI-2004-RepsSY #implementation: Symbolic Implementation of the Best Transformer (TWR, SS, GY), pp. 252–266.
CC-2003-MelskiR #interprocedural: The Interprocedural Express-Lane Transformation (DM, TWR), pp. 200–216.
ESOP-2003-RepsSL #difference #finite #logic #static analysis: Finite Differencing of Logical Formulas for Static Analysis (TWR, SS, AL), pp. 380–398.
ESOP-2003-YahavRSW #evolution #logic #verification: Verifying Temporal Heap Properties Specified via Evolution Logic (EY, TWR, SS, RW), pp. 204–222.
SAS-2003-RepsSJ #analysis #automaton #data flow #interprocedural: Weighted Pushdown Systems and Their Application to Interprocedural Dataflow Analysis (TWR, SS, SJ), pp. 189–213.
LICS-2002-RepsLS #semantics: Semantic Minimization of 3-Valued Propositional Formulae (TWR, AL, SS), p. 40–?.
SAS-2002-Reps #logic #program analysis: Static Program Analysis via 3-Valued Logic (TWR), p. 1.
ESOP-2001-XuRM #type system: Typestate Checking of Machine Code (ZX, TWR, BPM), pp. 335–351.
FASE-2001-LoginovYHR #debugging #runtime #type checking: Debugging via Run-Time Type Checking (AL, SHY, SH, TWR), pp. 217–232.
ICALP-2001-BenediktGR #model checking #state machine #strict: Model Checking of Unrestricted Hierarchical State Machines (MB, PG, TWR), pp. 652–666.
CC-2000-WilhelmSR #analysis: Shape Analysis (RW, SS, TWR), pp. 1–17.
ISSTA-2000-Lev-AmiRSW #case study #static analysis #verification: Putting static analysis to work for verification: A case study (TLA, TWR, SS, RW), pp. 26–38.
PLDI-2000-XuMR #safety: Safety checking of machine code (ZX, BPM, TWR), pp. 70–82.
CC-1999-MelskiR #interprocedural #profiling: Interprocedural Path Profiling (DM, TWR), pp. 47–62.
ESEC-FSE-1999-SiffCBKR #c: Coping with Type Casts in C (MS, SC, TB, KK, TWR), pp. 180–198.
ESOP-1999-BenediktRS #data type #decidability #linked data #logic #open data: A Decidable Logic for Describing Linked Data Structures (MB, TWR, SS), pp. 2–19.
PASTE-1999-ChandraR #c #physics #type checking: Physical Type Checking for C (SC, TWR), pp. 66–75.
PLDI-1999-YongHR #analysis #pointer #source code: Pointer Analysis for Programs with Structures and Casting (SHY, SH, TWR), pp. 91–103.
POPL-1999-SagivRW #analysis #logic #parametricity: Parametric Shape Analysis via 3-Valued Logic (SS, TWR, RW), pp. 105–118.
ESEC-FSE-1997-RepsBDL #maintenance #problem #profiling #using: The Use of Program Profiling for Software Maintenance with Applications to the Year 2000 Problem (TWR, TB, MD, JRL), pp. 432–449.
ICSM-1997-SiffR #concept analysis #identification: Identifying modules via concept analysis (MS, TWR), pp. 170–179.
ILPS-1997-Reps #graph #program analysis #reachability: Program Analysis via Graph Reachability (TWR), pp. 5–19.
PEPM-1997-MelskiR #constraints #context-free grammar #reachability #set: Interconveritibility of Set Constraints and Context-Free Language Reachability (DM, TWR), pp. 74–89.
FSE-1996-SiffR #c #c++ #reuse: Program Generalization for Software Reuse: From C to C++ (MS, TWR), pp. 135–146.
POPL-1996-SagivRW #problem: Solving Shape-Analysis Problems in Languages with Destructive Updating (SS, TWR, RW), pp. 16–31.
FSE-1995-HorwitzRS #analysis #data flow #interprocedural: Demand Interprocedural Dataflow Analysis (SH, TWR, SS), pp. 104–115.
FSE-1995-RepsR #interprocedural #precise: Precise Interprocedural Chopping (TWR, GR), pp. 41–52.
PEPM-1995-DasRH #analysis #imperative #semantics #source code: Semantic Foundations of Binding Time Analysis for Imperative Programs (MD, TWR, PVH), pp. 100–110.
PEPM-1995-Reps #analysis #problem: Shape Analysis as a Generalized Path Problem (TWR), pp. 1–11.
POPL-1995-RepsHS #analysis #data flow #graph #interprocedural #precise #reachability: Precise Interprocedural Dataflow Analysis via Graph Reachability (TWR, SH, SS), pp. 49–61.
CC-1994-Reps #analysis #interprocedural #problem: Solving Demand Versions of Interprocedural Analysis Problems (TWR), pp. 389–403.
FSE-1994-RepsHSR #slicing: Speeding up Slicing (TWR, SH, SS, GR), pp. 11–20.
POPL-1994-RamalingamR #algorithm #incremental #maintenance: An Incremental Algorithm for Maintaining the Dominator Tree of a Reducible Flowgraph (GR, TWR), pp. 287–296.
POPL-1993-RamalingamR #incremental #overview: A Categorized Bibliography on Incremental Computation (GR, TWR), pp. 502–510.
ICSE-1992-HorwitzR #dependence #graph #re-engineering #using: The Use of Program Dependence Graphs in Software Engineering (SH, TWR), pp. 392–411.
ESOP-1990-Reps #algebra #integration: Algebraic Properties of Program Integration (TWR), pp. 326–340.
ESOP-J-1990-Reps91 #algebra #integration: Algebraic Properties of Program Integration (TWR), pp. 139–215.
PLDI-1989-HorwitzPR #analysis #dependence #pointer: Dependence Analysis for Pointer Variables (SH, PP, TWR), pp. 28–40.
Best-of-PLDI-1988-HorwitzRB88a #dependence #graph #interprocedural #slicing #using: Interprocedural slicing using dependence graphs (with retrospective) (SH, TWR, DB), pp. 229–243.
ESOP-1988-RepsH #integration #semantics: Semantics-Based Program Integration (TWR, SH), pp. 1–20.
PLDI-1988-HorwitzRB #dependence #graph #interprocedural #slicing #using: Interprocedural Slicing Using Dependence Graphs (SH, TWR, DB), pp. 35–46.
POPL-1988-HorwitzPR #source code: Integrating Non-Interfering Versions of Programs (SH, JP, TWR), pp. 133–145.
POPL-1988-HorwitzPR88a #dependence #graph #on the #representation #source code: On the Adequacy of Program Dependence Graphs for Representing Programs (SH, JP, TWR), pp. 146–157.
POPL-1986-RepsMT #editing: Remote Attribute Updating for Language-Based Editors (TWR, CM, TT), pp. 1–13.
POPL-1984-RepsA #interactive #proving: Interactive Proof Checking (TWR, BA), pp. 36–45.
POPL-1982-Reps #analysis #editing #incremental #semantics: Optimal-Time Incremental Semantic Analysis for Syntax-Directed Editors (TWR), pp. 169–176.
POPL-1981-DemersRT #attribute grammar #editing #incremental: Incremental Evaluation for Attribute Grammars with Application to Syntax-Directed Editors (AJD, TWR, TT), pp. 105–116.
ESEC-FSE-2017-BrownVLR: The care and feeding of wild-caught mutants (DBB, MV, BL, TWR), pp. 511–522.
ESEC-FSE-2018-HenkelLLR #comprehension #embedded #source code: Code vectors: understanding programs through embedded abstracted symbolic traces (JH, SKL, BL, TWR), pp. 163–174.
CCIPL-1989-RepsY #integration #semantics #slicing: The Semantics of Program Slicing and Program Integration (TWR, WY), pp. 360–374.
CCPSD-1991-RamalingamR #formal method: A Theory of Program Modifications (GR, TWR), pp. 137–152.
TAPSOFT-1995-SagivRH #analysis #constant #data flow #interprocedural #precise: Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation (SS, TWR, SH), pp. 651–665.
TAPSOFT-J-1995-SagivRH96 #analysis #constant #data flow #interprocedural #precise: Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation (SS, TWR, SH), pp. 131–170.
ESOP-2016-MineBR #algorithm #constraints #induction #invariant #source code #theorem proving: An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs (AM, JB, TWR), pp. 560–588.
CAV-2017-Carbonneaux0RS #analysis #automation #coq #proving: Automated Resource Analysis with Coq Proof Objects (QC, JH0, TWR, ZS), pp. 64–85.
CAV-2019-HuBCDR #proving #synthesis: Proving Unrealizability for Syntax-Guided Synthesis (QH, JB, JC, LD, TWR), pp. 335–352.
OOPSLA-2016-SrinivasanR #algorithm #slicing: An improved algorithm for slicing machine code (VS, TWR), pp. 378–393.
OOPSLA-2016-SrinivasanSR #synthesis: Speeding up machine-code synthesis (VS, TS, TWR), pp. 165–180.
OOPSLA-2017-SrinivasanVR #synthesis: Model-assisted machine-code synthesis (VS, AV, TWR), p. 26.
POPL-2016-RepsTP #program analysis: Newtonian program analysis via tensor product (TWR, ET, PP), pp. 663–677.
PLDI-2017-KincaidBBR #analysis #composition #revisited: Compositional recurrence analysis revisited (ZK, JB, AFB, TWR), pp. 248–262.
POPL-2017-FengM0DR #api #component #synthesis: Component-based synthesis for complex APIs (YF, RM, YW0, ID, TWR), pp. 599–612.
PLDI-2018-WangHR #algebra #framework #named #probability #source code #static analysis: PMAF: an algebraic framework for static analysis of probabilistic programs (DW, JH0, TWR), pp. 513–528.
POPL-2018-KincaidCBR #invariant #reasoning #synthesis: Non-linear reasoning for invariant synthesis (ZK, JC, JB, TWR), p. 33.
POPL-2019-CyphertBKR #refinement #static analysis: Refinement of path expressions for static analysis (JC, JB, ZK, TWR), p. 29.
POPL-2019-KincaidBCR: Closed forms for numerical loops (ZK, JB, JC, TWR), p. 29.