Titre :

Static Analysis Of Binary Code With Memory Indirections Using Polyhedra

Auteur(s) :

Ballabriga, Clement [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Forget, Julien [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Gonnord, Laure [Auteur]
Université Claude Bernard Lyon 1 [UCBL]
CASH - Compilation and Analysis, Software and Hardware [CASH]
Laboratoire de l'Informatique du Parallélisme [LIP]
Lipari, Giuseppe [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Ruiz, Jordy [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]

Titre de la manifestation scientifique :

VMCAI'19 - International Conference on Verification, Model Checking, and Abstract Interpretation

Ville :

Cascais

Pays :

Portugal

Date de début de la manifestation scientifique :

2019-01-13

Titre de la revue :

LNCS

Éditeur :

Springer

Mot(s)-clé(s) en anglais :

binary analysis
Worst-case Execution Time WCET
polyhedra

Discipline(s) HAL :

Informatique [cs]/Informatique et langage [cs.CL]
Informatique [cs]/Algorithme et structure de données [cs.DS]
Informatique [cs]/Systèmes embarqués

Résumé en anglais : [en]

In this paper we propose a new abstract domain for staticanalysis of binary code. Our motivation stems from the need to improve the precision of the estimation of the Worst-Case Execution Time(WCET) of safety-critical ...
Lire la suite >In this paper we propose a new abstract domain for staticanalysis of binary code. Our motivation stems from the need to improve the precision of the estimation of the Worst-Case Execution Time(WCET) of safety-critical real-time code. WCET estimation requires computing information such as upper bounds on the number of loop iterations, unfeasible execution paths, etc. These estimations are usually performed on binary code, mainly to avoid making assumptions on how the compiler works. Our abstract domain, based on polyhedra and on two mapping functions that associate polyhedra variables with registers and memory, targets the precise computation of such information. We prove the correctness of the method, and demonstrate its effectiveness on benchmarks and examples from typical embedded code.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Projet ANR :

Ordonnancement de programmes à structures de données complexes
Une méthodologie correcte par construction pour supporter la variabilité du temps d'exécution dans les systèmes temps réel

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL