Sciweavers

15 search results - page 3 / 3
» vmcai 2007
Sort
View
VMCAI
2007
Springer
13 years 11 months ago
Constraint Solving for Interpolation
Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing separation between the sets of ‘good...
Andrey Rybalchenko, Viorica Sofronie-Stokkermans
VMCAI
2007
Springer
13 years 11 months ago
Shape Analysis of Single-Parent Heaps
We define the class of single-parent heap systems, which rely on a singly-linked heap in order to model destructive updates on tree structures. This encoding has the advantage of ...
Ittai Balaban, Amir Pnueli, Lenore D. Zuck
VMCAI
2007
Springer
13 years 11 months ago
DIVINE: DIscovering Variables IN Executables
Abstract. This paper addresses the problem of recovering variable-like entities when analyzing executables in the absence of debugging information. We show that variable-like entit...
Gogul Balakrishnan, Thomas W. Reps
VMCAI
2007
Springer
13 years 11 months ago
Better Under-Approximation of Programs by Hiding Variables
Abstraction frameworks use under-approximating transitions in order to prove existential properties of concrete systems. Under-approximating transifer to the concrete states that c...
Thomas Ball, Orna Kupferman
VMCAI
2007
Springer
13 years 11 months ago
Lattice Automata
Abstract. Several verification methods involve reasoning about multi-valued systems, in which an atomic proposition is interpreted at a state as a lattice element, rather than a B...
Orna Kupferman, Yoad Lustig