CAV
2007
Springer
14 years 7 months ago
2007
Springer
We present new techniques for fast, accurate and scalable static data race detection in concurrent programs. Focusing our analysis on Linux device drivers allowed us to identify th...
CAV
2007
Springer
14 years 7 months ago
2007
Springer
Liveness temporal properties state that something “good” eventually happens, e.g., every request is eventually granted. In Linear Temporal Logic (LTL), there is no a priori bo...
CAV
2007
Springer
14 years 7 months ago
2007
Springer
CAV
2007
Springer
14 years 7 months ago
2007
Springer
CAV
2007
Springer
14 years 7 months ago
2007
Springer
Abstract. TVLA is a parametric framework for shape analysis that can be easily instantiated to create different kinds of analyzers for checking properties of programs that use link...
CAV
2007
Springer
14 years 7 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 7 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 7 months ago
2007
Springer
CAV
2007
Springer
14 years 7 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 7 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...