Now showing items 48-67 of 95

    • On Generalized Authorization Problems 

      Schwoon, Stefan; Jha, Somesh; Reps, Thomas; Stubblebine, S. (University of Wisconsin-Madison Department of Computer Sciences, 2003)
      This paper defines a framework in which one can formalize a variety of authorization and policy issues that arise in access control of shared computing resources. Instantiations of the framework address such issues as ...
    • On the Adequacy of Program Dependence Graphs for Representing Programs 

      Horwitz, Susan; Prins, Jan; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 1987)
    • On the Algebraic Properties of Program Integration 

      Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 1989)
    • On the Computational Complexity of Incremental Algorithms 

      Ramalingam, G; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 1991)
    • Parametric Shape Analysis via 3-Valued Logic 

      Sagiv, Mooly; Reps, Thomas; Wilhelm, Reinhard (University of Wisconsin-Madison Department of Computer Sciences, 1998)
    • Partial Evaluation of Machine Code 

      Srinivasan, Venkatesh; Reps, Thomas (2015-08-21)
      This paper presents an algorithm for off-line partial evaluation of machine code. The algorithm follows the classical two-phase approach of binding-time analysis (BTA) followed by specialization. However, machine-code ...
    • PostHat and All That: Attaining Most-Precise Inductive Invariants 

      Reps, Thomas; Lim, Junghee; Lal, Akash; Thakur, Aditya (2013-04-16)
      In abstract interpretation, the choice of an abstract domain fixes a limit on the precision of the inductive invariants that one can express; however, for a given abstract domain A, there is a most-precise (``strongest'', ...
    • Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation 

      Sagiv, Mooly; Reps, Thomas; Horwitz, Susan (University of Wisconsin-Madison Department of Computer Sciences, 1995)
    • Program Analysis via Graph Reachability 

      Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 1998)
    • Program Generalization for Software Reuse: From C to C++ 

      Siff, Michael; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 1996)
    • Program Specialization via Program Slicing 

      Reps, Thomas; Turnidge, Todd (University of Wisconsin-Madison Department of Computer Sciences, 1995)
    • Programming for a Capability System via Safety Games 

      Harris, William R.; Farley, Benjamin; Jha, Somesh; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2011)
      New operating systems with security-specific system calls, such as the Capsicum capability system, allow programmers to write applications that satisfy strong security properties with significantly less effort than full ...
    • Programming for a Capability System via Safety Games 

      Farley, Benjamin; Harris, William; Reps, Thomas; Jha, Somesh (2012-04-05)
      New operating systems with security-specific system calls, such as the Capsicum capability system, allow programmers to write applications that satisfy strong security properties with significantly less effort than full ...
    • Property-Directed Shape Analysis 

      Itzhaky, Shachar; Bjorner, Nikolaj; Reps, Thomas; Sagiv, Mooly; Thakur, Aditya (2014-05-22)
      This paper addresses the problem of automatically generating quantified invariants for programs that manipulate singly and doubly linked-list data structures. Our algorithm is property-directed -- i.e., its choices are ...
    • Recency-Abstraction for Heap-Allocated Storage 

      Balakrishnan, Gogul; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2005)
      In this paper, we present an abstraction for heap-allocated storage, called the recency-abstraction, that allows abstract-interpretation algorithms to recover non-trivial information for heap-allocated data objects. As an ...
    • Recovery of Variables and Heap Structure in x86 Executables 

      Balakrishnan, Gogul; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2005)
      This paper addresses two problems that arise when analyzing executables: (1) recovering variable-like quantities in the absence of symbol-table and debugging information, and (2) recovering useful information about objects ...
    • Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis 

      Lal, Akash; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2008)
      This paper addresses the analysis of concurrent programs with shared memory. Such an analysis is undecidable in the presence of multiple procedures. One approach used in recent work obtains decidability by providing only ...
    • Reducing the Dependence of Trust-Management Systems on PKI 

      Wang, Hao; Jha, Somesh; Reps, Thomas; Schwoon, Stefan; Stubblebine, Stuart (University of Wisconsin-Madison Department of Computer Sciences, 2005)
      Trust-management systems address the authorization problem in distributed systems by defining a formal language for expressing authorization and access-control policies, and relying on an algorithm to determine when a ...
    • A Relational Approach to Interprocedural Shape Analysis 

      Jeannet, Bertrand; Loginov, Alexey; Reps, Thomas; Sagiv, Mooly (University of Wisconsin-Madison Department of Computer Sciences, 2004)
      This paper addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields-i.e., interprocedural shape analysis. ...
    • Satisfiability Modulo Abstraction for Separation Logic with Linked Lists 

      Thakur, Aditya; Breck, Jason; Reps, Thomas (University of Wisconsin-Madison Department of Computer Sciences, 2014-07-17)
      Separation logic is an expressive logic for reasoning about heap structures in programs. This paper presents a semi-decision procedure for checking unsatisfiability of formulas in a fragment of separation logic that includes ...