Preventing Arithmetic Overflows in Alloy
In a bounded analysis, arithmetic operators become partial, and a different semantics becomes necessary. One approach, mimicking programming languages, is for overflow to result in wrap-around. Although easy to implement, wrap-around produces unexpected counterexamples that do not correspond to case...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Springer-Verlag
2014
|
| Online Access: | http://hdl.handle.net/1721.1/86925 https://orcid.org/0000-0003-4864-078X |
| _version_ | 1826192551898513408 |
|---|---|
| author | Milicevic, Aleksandar Jackson, Daniel |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Milicevic, Aleksandar Jackson, Daniel |
| author_sort | Milicevic, Aleksandar |
| collection | MIT |
| description | In a bounded analysis, arithmetic operators become partial, and a different semantics becomes necessary. One approach, mimicking programming languages, is for overflow to result in wrap-around. Although easy to implement, wrap-around produces unexpected counterexamples that do not correspond to cases that would arise in the unbounded setting. This paper describes a new approach, implemented in the latest version of the Alloy Analyzer, in which instances that would involve overflow are suppressed, and consequently, spurious counterexamples are eliminated. The key idea is to interpret quantifiers so that bound variables range only over values that do not cause overflow. |
| first_indexed | 2024-09-23T09:19:17Z |
| format | Article |
| id | mit-1721.1/86925 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T09:19:17Z |
| publishDate | 2014 |
| publisher | Springer-Verlag |
| record_format | dspace |
| spelling | mit-1721.1/869252022-09-30T14:13:48Z Preventing Arithmetic Overflows in Alloy Milicevic, Aleksandar Jackson, Daniel Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Milicevic, Aleksandar Jackson, Daniel In a bounded analysis, arithmetic operators become partial, and a different semantics becomes necessary. One approach, mimicking programming languages, is for overflow to result in wrap-around. Although easy to implement, wrap-around produces unexpected counterexamples that do not correspond to cases that would arise in the unbounded setting. This paper describes a new approach, implemented in the latest version of the Alloy Analyzer, in which instances that would involve overflow are suppressed, and consequently, spurious counterexamples are eliminated. The key idea is to interpret quantifiers so that bound variables range only over values that do not cause overflow. 2014-05-09T18:35:54Z 2014-05-09T18:35:54Z 2012-06 Article http://purl.org/eprint/type/ConferencePaper 978-3-642-30884-0 978-3-642-30885-7 0302-9743 1611-3349 http://hdl.handle.net/1721.1/86925 Milicevic, Aleksandar, and Daniel Jackson. “Preventing Arithmetic Overflows in Alloy.” Lecture Notes in Computer Science (2012): 108–121. https://orcid.org/0000-0003-4864-078X en_US http://dx.doi.org/10.1007/978-3-642-30885-7_8 Abstract State Machines, Alloy, B, VDM, and Z Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Springer-Verlag MIT web domain |
| spellingShingle | Milicevic, Aleksandar Jackson, Daniel Preventing Arithmetic Overflows in Alloy |
| title | Preventing Arithmetic Overflows in Alloy |
| title_full | Preventing Arithmetic Overflows in Alloy |
| title_fullStr | Preventing Arithmetic Overflows in Alloy |
| title_full_unstemmed | Preventing Arithmetic Overflows in Alloy |
| title_short | Preventing Arithmetic Overflows in Alloy |
| title_sort | preventing arithmetic overflows in alloy |
| url | http://hdl.handle.net/1721.1/86925 https://orcid.org/0000-0003-4864-078X |
| work_keys_str_mv | AT milicevicaleksandar preventingarithmeticoverflowsinalloy AT jacksondaniel preventingarithmeticoverflowsinalloy |