Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration (extended version)

Colas Le Guernic 1, 2
2 TAMIS - Threat Analysis and Mitigation for Information Security
Inria Rennes – Bretagne Atlantique , IRISA_D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : In a POPL 2014 paper, Jeannet et al. showed that abstract acceleration is a relevant approach for general linear loops thanks to the Jordan decomposition of the linear transformer. Bounding the number of loop iterations involves interval-linear constraints. After identifying sources of over-approximation, we present some improvements over their method. First, we improve precision by using interval hulls in the Jordan parameters space instead of the state space, avoiding further interval arithmetic. Then, we show how to use conic hulls instead of interval hulls to further improve precision. Furthermore, we extend their work to handle linear loops with bounded nondeterministic input. This was already attempted by Cattaruzza et al. in a SAS 2015 paper, unfortunately their method is unsound. After explaining why, we propose a sound approach to guarded LTI loops with bounded nondeterministic inputs by reduction to the autonomous case.
Type de document :
Communication dans un congrès
Static Analysis Symposium, Aug 2017, New York, United States. 10422, Lecture Notes in Computer Science. 〈http://staticanalysis.org/sas2017/〉
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01550767
Contributeur : Colas Le Guernic <>
Soumis le : jeudi 29 juin 2017 - 17:37:56
Dernière modification le : jeudi 15 novembre 2018 - 11:58:59
Document(s) archivé(s) le : lundi 22 janvier 2018 - 18:49:23

Fichier

SoundAbsAccLTI.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

  • HAL Id : hal-01550767, version 1

Citation

Colas Le Guernic. Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration (extended version). Static Analysis Symposium, Aug 2017, New York, United States. 10422, Lecture Notes in Computer Science. 〈http://staticanalysis.org/sas2017/〉. 〈hal-01550767〉

Partager

Métriques

Consultations de la notice

468

Téléchargements de fichiers

126