Sound numerical computations in abstract acceleration

  • Cattaruzza, D
  • Abate, A
  • Schrammel, P
  • Kroening, D
ORKG logo Add to ORKG
Publication date
January 2017
Publisher
Springer Verlag

Abstract

Soundness is a major objective for verification tools. Methods that use exact arithmetic or symbolic representations are often prohibitively slow and do not scale past small examples. We propose the use of numerical oating-point computations to improve performance combined with an interval analysis to ensure soundness in reach-set computations for numerical dynamical models. Since the interval analysis cannot provide exact answers we reason about over-approximations of the reachable sets that are guaranteed to contain the true solution of the problem. Our theory is implemented in a numerical algorithm for Abstract Acceleration in a tool called Axelerator. Experimental results show a large increase in performance while maintaining soundness...

Extracted data

Loading...

Related items

Acceleration of the abstract fixpoint computation in numerical program analysis
  • Bouissou, Olivier
  • Seladji, Yassamine
  • Chapoutot, Alexandre
December 2012

International audienceStatic analysis by abstract interpretation aims at automatically proving prope...

Abstract Fixpoint Computations with Numerical Acceleration Methods
  • Bouissou, Olivier
  • Seladji, Yassamine
  • Chapoutot, Alexandre
October 2010

AbstractStatic analysis by abstract interpretation aims at automatically proving properties of compu...

Extending Abstract Acceleration Methods to Data-Flow Programs with Numerical Inputs
  • Schrammel, Peter
  • Jeannet, Bertrand
October 2010

AbstractAcceleration methods are commonly used for computing precisely the effects of loops in the r...

We use cookies to provide a better user experience.