Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Colas Le Guernic Connect in order to contact the contributor
Submitted on : Thursday, June 29, 2017 - 5:37:56 PM
Last modification on : Monday, April 4, 2022 - 9:28:22 AM
Long-term archiving on: : Monday, January 22, 2018 - 6:49:23 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License


  • HAL Id : hal-01550767, version 1


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. ⟨hal-01550767⟩



Record views


Files downloads