-
A constraint-based algorithm for analysing memory usage on Java cards
We address in this paper the problem of statically determining whether a JavaCard applet may produce a memory overflow because of the dynamic instantiation of classes... -
Taking architecture and compiler into account in formal proofs of numerical p...
On some recently developed architectures, a numerical program may give different answers depending on the execution hardware and the compilation. These discrepancies... -
Dexpler: Converting Android Dalvik Bytecode to Jimple for Static Analysis wit...
International audience -
Abstract acceleration in Linear relation analysis
{Linear Relation Analysis~\cite{cousot78,halbwach79} is now a classical abstract interpretation based on an approximation of reachable numerical states of a program by... -
Abstract Acceleration in Linear relation analysis (extended version)
Linear relation analysis is a classical abstract interpretation based on an over-approximation of reachable numerical states of a program by convex polyhedra. Since it... -
Performance prediction of distributed computing applications executed on a pe...
In the field of high performance computing, the architectures evolve continuously. In order to increase the number of computing nodes or the network speed, an... -
Rank: a tool to check program termination and computational complexity
International audience -
Automatically Securing Permission-Based Software by Reducing the Attack Surfa...
A common security architecture, called the permission-based security model (used e.g. in Android and Blackberry), entails intrinsic risks. For instance, applications... -
Efficient Generation of Correctness Certificates for the Abstract Domain of P...
International audience -
Logico-Numerical Verification Methods for Discrete and Hybrid Systems
This thesis studies the automatic verification of safety properties of logico-numerical discrete and hybrid systems. These systems have Boolean and numerical variables... -
Static Analysis
International audience -
A verifiable Lightweight Escape Analysis Supporting Creational Design Patterns
This paper presents a compositional escape analysis adapted for use in resource limited embedded systems. This analysis covers the full Java language, including... -
Towards efficient and secure shared memory applications
The invasion of multi-core and multi-processor platforms on all aspects of computing makes shared memory parallel programming mainstream. Yet, the fundamental problems... -
Tree Automata Completion for Static Analysis of Functional Programs
Tree Automata Completion is a family of techniques for computing or approximating the set of terms reachable by a rewriting relation. For functional programs... -
Static Analysis of Semantic Web Queries
Query containment is a well-studied problem spanning over several decades of research. Generally, it is defined as the problem of determining if the result of one... -
Static Analysis using Parameterised Boolean Equation Systems
Submitted to an international 2006 conference -
Classification of errors threats by static analysis, program sclicing and str...
Software validation remains a crucial part in software development process. Two major techniques have improved in recent years, dynamic and static analysis. They have... -
Analysis of probabilistic programs by abstract interpretation
version corrigée de quelques scories -
The ASTRÉE analyzer
Astrée is an abstract interpretation-based static program analyzer aiming at proving automatically the absence of run time errors in programs written in the C...
