-
Modular termination of C programs
In this paper we describe a general method to prove termination of C programs in a scalable and modular way. The program to analyse is reduced to the smallest relevant... -
Calculation of Worst Case Execution Time safe upper bounds for hard real-time...
This report is a presentation of a new approach for Worst Case Execu- tion Time (WCET) computation for hard real-time systems, especially for cache memories hazard... -
A New Abstract Domain for the Representation of Mathematically Equivalent Exp...
International audience -
TAPENADE 2.1 user's guide
This is the user's manual for the version 2.1 of the Automatic Differentiation tool TAPENADE. Given a source computer program that computes a differentiable... -
Improving privacy on android smartphones through in-vivo bytecode instrumenta...
In this paper we claim that a widely applicable and efficient means to fight against malicious mobile Android applications is: 1) to per- form runtime monitoring 2) by... -
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...
