Now showing items 1-10 of 10

    • 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 ...
    • Demand Interprocedural Dataflow Analysis 

      Horwitz, Susan; Reps, Thomas; Sagiv, Mooly (University of Wisconsin-Madison Department of Computer Sciences, 1995)
    • LTL Model Checking for Systems with Unbounded Number of Dynamically Created Threads and Objects, 

      Yahav, Eran; Reps, Thomas; Sagiv, Mooly (University of Wisconsin-Madison Department of Computer Sciences, 2001)
    • Numeric Analysis of Array Operations 

      Gopan, Denis; Reps, Thomas; Sagiv, Mooly (University of Wisconsin-Madison Department of Computer Sciences, 2004)
      We present a numeric analysis that is capable of reasoning about array operations. In particular, the analysis is able to establish that all elements of an array have been initialized ("an array kill"), as well as to ...
    • Parametric Shape Analysis via 3-Valued Logic 

      Sagiv, Mooly; Reps, Thomas; Wilhelm, Reinhard (University of Wisconsin-Madison Department of Computer Sciences, 1998)
    • Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation 

      Sagiv, Mooly; Reps, Thomas; Horwitz, Susan (University of Wisconsin-Madison Department of Computer Sciences, 1995)
    • 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 ...
    • 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. ...
    • Solving Shape-Analysis Problems in Languages with Destructive Updating 

      Sagiv, Mooly; Reps, Thomas; Wilhelm, Reinhard (University of Wisconsin-Madison Department of Computer Sciences, 1996)
    • Symbolic Implementation of the Best Transformer 

      Reps, Thomas; Sagiv, Mooly; Yorsh, Greta (University of Wisconsin-Madison Department of Computer Sciences, 2003)
      This paper shows how to achieve, under certain conditions, abstract-interpretation algorithms that enjoy the best possible precision for a given abstraction. The key idea is a simple process of successive approximation ...