VSTTE
2010
Springer
13 years 10 months ago
2010
Springer
Abstract. Theorem-prover based modular checkers have the potential to perform scalable and precise checking of user-defined properties by combining pathsensitive intraprocedural re...
VSTTE
2010
Springer
13 years 10 months ago
2010
Springer
VSTTE
2010
Springer
13 years 10 months ago
2010
Springer
A suite of verification benchmarks for software verification tools and techniques, presented at VSTTE 2008 [11], provides an initial catalogue of benchmark challenges for the Verif...
VSTTE
2010
Springer
13 years 10 months ago
2010
Springer
Garbage collectors are very hard to implement correctly due to their low-level manipulation of memory. In this paper, we construct a copying garbage collector which we have proved ...
VSTTE
2010
Springer
13 years 10 months ago
2010
Springer
Formal modeling of computing systems yields models that are intended to be correct with respect to the requirements that have been formalized. The complexity of typical computing s...
VSTTE
2010
Springer
13 years 10 months ago
2010
Springer
Abstract. The Composite design pattern is an exemplar of specification and verification challenges for sequential object-oriented programs. Region logic is a Hoare logic augmente...
VSTTE
2010
Springer
13 years 10 months ago
2010
Springer
VSTTE
2010
Springer
13 years 10 months ago
2010
Springer
Abstract. This paper presents a method for deriving an expression from the lowlevel code compiled from an expression in a high-level language. The input is a low-level control flo...