-
Applying abstract acceleration to (co-)reachability analysis of reactive prog...
International audience -
Logico-Numerical Abstract Acceleration and Application to the Verification of...
Acceleration methods are commonly used for speeding up the convergence of loops in reachability analysis of counter machine models. Applying these methods to... -
Logico-Numerical Max-Strategy Iteration
International audience -
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...
