VMCAI
2007
Springer
13 years 11 months ago
2007
Springer
We present a constraint-based algorithm for the synthesis of invariants expressed in the combined theory of linear arithmetic and uninterpreted function symbols. Given a set of pro...
VMCAI
2007
Springer
13 years 11 months ago
2007
Springer
Abstraction frameworks use under-approximating transitions in order to prove existential properties of concrete systems. Under-approximating transifer to the concrete states that c...
VMCAI
2007
Springer
13 years 11 months ago
2007
Springer
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...
VMCAI
2007
Springer
13 years 11 months ago
2007
Springer
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 ...
VMCAI
2007
Springer
13 years 11 months ago
2007
Springer