AMAST
2008
Springer
13 years 6 months ago
2008
Springer
Abstract. We present a static analysis technique for modeling and approximating the long-run resource usage of programs. The approach is based on a quantitative semantic framework ...
AMAST
2008
Springer
13 years 6 months ago
2008
Springer
Several proof systems allow the formal verification of Java programs, and a specification language was specifically designed for Java. However, none of these systems support generi...
AMAST
2008
Springer
13 years 6 months ago
2008
Springer
Many complex analysis problems can be most clearly and easily specified as logic rules and queries, where rules specify how given facts can be combined to infer new facts, and quer...
AMAST
2008
Springer
13 years 6 months ago
2008
Springer
In this paper, we present a novel approach that establishes a synergy between static and dynamic analyses for detecting memory errors in C code. We extend the standard C type syste...
AMAST
2008
Springer
13 years 6 months ago
2008
Springer
AMAST
2008
Springer
13 years 6 months ago
2008
Springer
The complexity of specification development and verification of large systems has to be mastered. In this paper a specification of a real case study, a platoon of Cristal vehicles ...
AMAST
2008
Springer
13 years 6 months ago
2008
Springer
The authors have proposed using category-theoretic sketches to enhance database design and integration methodologies. The algebraic context is called the Sketch Data Model (SkDM) a...
AMAST
2008
Springer
13 years 6 months ago
2008
Springer
Feature-Oriented Software Development (FOSD) provides a multitude of formalisms, methods, languages, and tools for building variable, customizable, and extensible software. Along d...
AMAST
2008
Springer
13 years 6 months ago
2008
Springer
Abstract. Vx86 is the first static analyzer for sequential Intel x86 assembler code using automated deductive verification. It proves the correctness of assembler code against func...
AMAST
2008
Springer
13 years 6 months ago
2008
Springer
We demonstrate Spiral, a domain-specific library generation system. Spiral generates high performance source code for linear transforms (such as the discrete Fourier transform and ...