Browsing by Author "Sagiv, Mooly"
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 ...