Sciweavers

AMAST
2008
Springer
14 years 2 months ago
Long-Run Cost Analysis by Approximation of Linear Operators over Dioids
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 ...
David Cachera, Thomas P. Jensen, Arnaud Jobin, Pas...
AMAST
2008
Springer
14 years 2 months ago
Verification of Java Programs with Generics
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...
Kurt Stenzel, Holger Grandy, Wolfgang Reif
AMAST
2008
Springer
14 years 2 months ago
Generating Specialized Rules and Programs for Demand-Driven Analysis
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...
K. Tuncay Tekle, Katia Hristova, Yanhong A. Liu
AMAST
2008
Springer
14 years 2 months ago
A Hybrid Approach for Safe Memory Management in C
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...
Syrine Tlili, Zhenrong Yang, Hai Zhou Ling, Mourad...
AMAST
2008
Springer
14 years 2 months ago
Towards Validating a Platoon of Cristal Vehicles Using CSP||B
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 ...
Samuel Colin, Arnaud Lanoix, Olga Kouchnarenko, Je...
AMAST
2008
Springer
14 years 2 months ago
Implementing a Categorical Information System
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...
Michael Johnson, Robert D. Rosebrugh
AMAST
2008
Springer
14 years 2 months ago
An Algebra for Features and Feature Composition
Feature-Oriented Software Development (FOSD) provides a multitude of formalisms, methods, languages, and tools for building variable, customizable, and extensible software. Along d...
Sven Apel, Christian Lengauer, Bernhard Mölle...
AMAST
2008
Springer
14 years 2 months ago
Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving
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...
Stefan Maus, Michal Moskal, Wolfram Schulte
AMAST
2008
Springer
14 years 2 months ago
System Demonstration of Spiral: Generator for High-Performance Linear Transform Libraries
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 ...
Yevgen Voronenko, Franz Franchetti, Fréd&ea...