SAS
2007
Springer
13 years 10 months ago
2007
Springer
Concurrent programs are difficult to verify because the proof must consider the interactions between the threads. Fine-grained concurrency and heap allocated data structures exacer...
SAS
2007
Springer
13 years 10 months ago
2007
Springer
Variables in programs are usually confined to a fixed number of bits and results that require more bits are truncated. Due to the use of 32-bit and 64-bit variables, inadvertent ...
SAS
2007
Springer
13 years 10 months ago
2007
Springer
Interval analysis seeks static lower and upper bounds on the values of program variables. These bounds are useful, especially for inferring invariants to prove buffer overflow ch...
SAS
2007
Springer
13 years 10 months ago
2007
Springer
Denotational static analysis of Java bytecode has a nice and clean compositional definition and an efficient implementation with binary decision diagrams. But it models only the f...
SAS
2007
Springer
13 years 10 months ago
2007
Springer
Abstract. Silicon chip design has passed a threshold whereby exponentially increasing transistor density (Moore’s Law) no longer translates into increased processing power for si...
SAS
2007
Springer
13 years 10 months ago
2007
Springer
abstraction on real-valued programs David Monniaux Laboratoire d’informatique de l’´Ecole normale sup´erieure 45, rue d’Ulm, 75230 Paris cedex 5, France June 30, 2007 In t...
SAS
2007
Springer
13 years 10 months ago
2007
Springer
Floating-point arithmetic is an important source of errors in programs because of the loss of precision arising during a computation. Unfortunately, this arithmetic is not intuitiv...
SAS
2007
Springer
13 years 10 months ago
2007
Springer
Abstract. Shape analyses are often imprecise in their numerical reasoning, whereas numerical static analyses are often largely unaware of the shape of a program’s heap. In this p...
SAS
2007
Springer
13 years 10 months ago
2007
Springer
SAS
2007
Springer
13 years 10 months ago
2007
Springer
