CAV
2007
Springer
14 years 5 months ago
2007
Springer
Abstract. We present an extrapolation with care set operator to accelerate termination of reachability computation with polyhedra. At the same time, a counterexample guided refine...
CAV
2007
Springer
14 years 5 months ago
2007
Springer
We propose a shape analysis that adapts to some of the complex composite data structures found in industrial systems-level programs. Examples of such data structures include “cyc...
CAV
2007
Springer
14 years 5 months ago
2007
Springer
CAV
2007
Springer
14 years 5 months ago
2007
Springer
Abstract. A temporal interface for a software component is a finite automaton that specifies the legal sequences of calls to functions that are provided by the component. We comp...
CAV
2007
Springer
14 years 5 months ago
2007
Springer
Programs typically make extensive use of libraries, including dynamically linked libraries, which are often not available in source-code form, and hence not analyzable by tools tha...
CAV
2007
Springer
14 years 5 months ago
2007
Springer
CAV
2007
Springer
14 years 5 months ago
2007
Springer
We present Hector, a software tool for combining different abstraction methods to extract sound models of heap-manipulating imperative programs with recursion. Extracted models ma...
CAV
2007
Springer
14 years 5 months ago
2007
Springer
Abstract. STP is a decision procedure for the satisfiability of quantifier-free formulas in the theory of bit-vectors and arrays that has been optimized for large problems encoun...
ASIAN
2007
Springer
14 years 5 months ago
2007
Springer
Abstract. This paper is concerned about relating formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first ord...
MEMOCODE
2008
IEEE
14 years 6 months ago
2008
IEEE
Equivalence checking is a classical verification method determining if a finite-state concurrent system (protocol) satisfies its desired external behaviour (service) by compari...