Browsing CS Technical Reports by Author "Reps, Thomas"

Now showing items 1-20 of 95

    • An Abstract Domain for Bit-Vector Inequalities 

      Reps, Thomas; Thakur, Aditya; Sharma, Tushar (University of Wisconsin-Madison Department of Computer Sciences, 2013-04-16)
      This paper advances the state of the art in abstract interpretation of machine code. It tackles two of the biggest challenges in machine-code analysis: (1) holding onto invariants about values in memory, and (2) identifying ...

    • Abstract Domains of Affine Relations 

      Elder, Matt; Lim, Junghee; Sharma, Tushar; Anderson, Tycho; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2013-05-13)
      This paper considers some known abstract domains for affine-relation analysis, along with several variants, and studies how they relate to each other. The various domains represent sets of points that satisfy affine ...

    • Abstract Domains of Affine Relations 

      Elder, Matt; Lim, Junghee; Sharma, Tushar; Andersen, Tycho; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2011)
      This paper considers some known abstract domains for affine-relation analysis (ARA), along with several variants, and studies how they relate to each other. We show that the abstract domains of Mueller-Olm/Seidl (MOS) ...

    • Abstract Error Projection 

      Lal, Akash; Kidd, Nicholas; Reps, Thomas; Touili, Tayssir (University of Wisconsin-Madison Department of Computer Sciences, 2006)
      To improve the reporting of results from model checking and programanalysis systems, we introduce the notion of an error projection and annotated error projection. An error projection is a set of program nodes N such that ...

    • Abstraction Refinement for 3-Valued Logic Analysis 

      Loginov, Alexey; Reps, Thomas; Sagiv, Mooly (University of Wisconsin-Madison Department of Computer Sciences, 2004)
      This paper concerns the question of how to create abstractions that are useful for program analysis. It presents a method that refines an abstraction automatically for analysis problems in which the semantics of statements ...

    • Advanced Querying for Property Checking 

      Kidd, Nicholas; Lal, Akash; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2007)
      Extended weighted pushdown systems (EWPDSs) are an extension of pushdown systems that incorporate infinite-state data abstractions. Nested-word automata (NWAs) are able to recognize languages that exhibit context-free ...

    • An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs 

      Mine, Antoine; Breck, Jason; Reps, Thomas (2016-01-08)
      This paper addresses the problem of proving a given invariance property phi of a loop in a numeric program, by inferring automatically a stronger inductive invariant psi. The algorithm we present is based on both abstract ...

    • Analyzing Memory Accesses in x86 Binary Executables 

      Balakrishnan, Gogul; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2003)
      This paper concerns static analysis algorithms for analyzing x86 executables. The aim of the work is to recover intermediate representations that are similar to those that can be created for a program written in a high-level ...

    • BCE: Extracting Botnet Commands from Bot Executables 

      Lim, Junghee; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2010)
      Botnets are a major threat to the security of computer systems and the Internet. An increasing number of individual Internet sites have been compromised by attacks from all across the world to become part of various kinds ...

    • Bilateral Algorithms for Symbolic Abstraction 

      Reps, Thomas; Elder, Matt; Thakur, Aditya (University of Wisconsin-Madison Department of Computer Sciences, 2012-03-28)
      Given a concrete domain C, a concrete operation tau: C -> C, and an abstract domain A, a fundamental problem in abstract interpretation is to find the best abstract transformer tau#: A -> A that over-approximates tau. ...

    • BTA Termination Using CFL-Reachability 

      Das, Manuvir; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 1996)

    • Compositional Recurrence Analysis Revisited 

      Kincaid, Zachary; Breck, Jason; Forouhi Boroujeni, Ashkan; Reps, Thomas (2017-03-08)
      Compositional recurrence analysis (CRA) is a static-analysis method based on a combination of symbolic analysis and abstract interpretation. This paper addresses the problem of creating a context-sensitive interprocedural ...

    • Computational Divided Differencing and Divided-Difference Arithmetics 

      Reps, Thomas; Rall, Louis (University of Wisconsin-Madison Department of Computer Sciences, 2000)

    • Correctness of an Algorithm for Reconstituting a Program From a Dependence Graph 

      Ball, Thomas; Horwitz, Susan; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 1990)

    • A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks 

      Kidd, Nicholas; Lammich, Peter; Touili, Tayssir; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2009)
      We present a new decision procedure for detecting property violations in pushdown models for concurrent programs that use lock-based synchronization, where each thread's lock operations are properly nested (a la ...

    • Declarative, Temporal, and Practical Programming with Capabilities 

      Watson, Robert N. M.; Anderson, Jonathan; Reps, Thomas; Jha, Somesh; Harris, William R. (2013-02-26)
      New operating systems, such as the Capsicum capability system, allow a programmer to write an application that satisfies strong security properties by invoking security- specific system calls at a few key points in the ...

    • Demand Interprocedural Dataflow Analysis 

      Horwitz, Susan; Reps, Thomas; Sagiv, Mooly (University of Wisconsin-Madison Department of Computer Sciences, 1995)

    • Demonstration of a Prototype Tool for Program Integration 

      Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 1989)
      This paper illustrates a sample session with a preliminary implementation of a program-integration tool. The tool has been embedded in a program editor created using the Synthesizer Generator, a meta-system for creating ...

    • Detecting Program Components With Equivalent Behaviors 

      Yang, Wuu; Horwitz, Susan; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 1989)
      The execution behavior of a program component is defined as the sequence of values produced at the component during program execution. This paper presents an efficient algorithm for detecting program components ? in one ...

    • DIFC Programs by Automatic Instrumentation 

      Harris, William; Jha, Somesh; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2010)
      Decentralized information flow control (DIFC) operating systems provide applications with mechanisms for enforcing information-flow policies for their data. However, significant obstacles keep such operating systems ...