Sound numerical computations in abstract acceleration

Conference item

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 of reachability results.

Authors: Cattaruzza, D; Abate, A; Schrammel, P; Kroening, D

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer Verlag
• Host title: Numerical Software Verification. NSV 2017. Lecture Notes in Computer Science
• Journal: NSV 2017: 10th International Workshop on Numerical Software Verification 2017, Heidelberg, Germany, July 22-23, 2017
• Volume: 10381
• Pages: 38-60
• Publication date: 2017-07-12
• Acceptance date: 2017-05-26
• DOI: 10.1007/978-3-319-63501-9_4
• ISSN: 0302-9743
• ISBN: 9783319635019