Sound numerical computations in abstract acceleration
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...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Published: |
Springer Verlag
2017
|
| _version_ | 1797073448384593920 |
|---|---|
| author | Cattaruzza, D Abate, A Schrammel, P Kroening, D |
| author_facet | Cattaruzza, D Abate, A Schrammel, P Kroening, D |
| author_sort | Cattaruzza, D |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T23:22:18Z |
| format | Conference item |
| id | oxford-uuid:69245401-e33b-4f2a-884e-0b33dee0bed2 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T23:22:18Z |
| publishDate | 2017 |
| publisher | Springer Verlag |
| record_format | dspace |
| spelling | oxford-uuid:69245401-e33b-4f2a-884e-0b33dee0bed22022-03-26T18:49:26ZSound numerical computations in abstract accelerationConference itemhttp://purl.org/coar/resource_type/c_5794uuid:69245401-e33b-4f2a-884e-0b33dee0bed2Symplectic Elements at OxfordSpringer Verlag2017Cattaruzza, DAbate, ASchrammel, PKroening, DSoundness 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. |
| spellingShingle | Cattaruzza, D Abate, A Schrammel, P Kroening, D Sound numerical computations in abstract acceleration |
| title | Sound numerical computations in abstract acceleration |
| title_full | Sound numerical computations in abstract acceleration |
| title_fullStr | Sound numerical computations in abstract acceleration |
| title_full_unstemmed | Sound numerical computations in abstract acceleration |
| title_short | Sound numerical computations in abstract acceleration |
| title_sort | sound numerical computations in abstract acceleration |
| work_keys_str_mv | AT cattaruzzad soundnumericalcomputationsinabstractacceleration AT abatea soundnumericalcomputationsinabstractacceleration AT schrammelp soundnumericalcomputationsinabstractacceleration AT kroeningd soundnumericalcomputationsinabstractacceleration |