CAV
2009
Springer
14 years 11 months ago
2009
Springer
We address the problem of analyzing programs such as J2ME midlets for mobile devices, where a central correctness requirement concerns confidentiality of data that the user wants t...
CAV
2009
Springer
14 years 11 months ago
2009
Springer
CAV
2009
Springer
14 years 11 months ago
2009
Springer
The SPEED project addresses the problem of computing symbolic computational complexity bounds of procedures in terms of their inputs. We discuss some of the challenges that arise a...
CAV
2009
Springer
14 years 11 months ago
2009
Springer
Abstract. Dynamic Pushdown Networks (DPNs) are a model for parallel programs with (recursive) procedures and process creation. The goal of this paper is to develop generic techniqu...
CAV
2009
Springer
14 years 11 months ago
2009
Springer
Abstract. We study the problem of determining, given a run of a concurrent program, whether there is any alternate execution of it that violates atomicity, where atomicity is defin...
CAV
2009
Springer
14 years 11 months ago
2009
Springer
Abstract. We propose a novel, sound, and complete Simplex-based algorithm for solving linear inequalities over integers. Our algorithm, which can be viewed as a semantic generaliza...
CAV
2009
Springer
14 years 11 months ago
2009
Springer
Context-bounded analysis is an attractive approach to verification of concurrent programs. Bounding the number of contexts executed per thread not only reduces the asymptotic compl...
CAV
2009
Springer
14 years 11 months ago
2009
Springer
CAV
2009
Springer
14 years 11 months ago
2009
Springer
Abstract. When a model does not satisfy a given specification, a counterexample is produced by the model checker to demonstrate the failure. A user must then examine the counterexa...
CAV
2009
Springer
14 years 11 months ago
2009
Springer
Quantifier reasoning in Satisfiability Modulo Theories (SMT) is a long-standing challenge. The practical method employed in modern SMT solvers is to instantiate quantified formulas...