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...
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...
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...
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...
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...
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...
Feature-Oriented Software Development (FOSD) provides a multitude of formalisms, methods, languages, and tools for building variable, customizable, and extensible software. Along d...
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...
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 ...