Accelerated Data-Flow Analysis

dc.creatorLeroux, Jérôme
dc.creatorSutre, Gregoire
dc.date2008-12-10
dc.date.accessioned2026-07-07T12:11:44Z
dc.date.available2026-07-07T12:11:44Z
dc.descriptionAcceleration in symbolic verification consists in computing the exact effect of some control-flow loops in order to speed up the iterative fix-point computation of reachable states. Even if no termination guarantee is provided in theory, successful results were obtained in practice by different tools implementing this framework. In this paper, the acceleration framework is extended to data-flow analysis. Compared to a classical widening/narrowing-based abstract interpretation, the loss of precision is controlled here by the choice of the abstract domain and does not depend on the way the abstract value is computed. Our approach is geared towards precision, but we don't loose efficiency on the way. Indeed, we provide a cubic-time acceleration-based algorithm for solving interval constraints with full multiplication.
dc.identifierhttps://arxiv.org/abs/0812.2011
dc.identifierhttp://arxiv.org/abs/0812.2011
dc.identifierStatic Analysis, Kongens Lyngby : Danemark (2007)
dc.identifierdoi:10.1007/978-3-540-74061-2_12
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/210317
dc.subjectData Structures and Algorithms
dc.titleAccelerated Data-Flow Analysis
dc.typetext

Files

Collections