mdh.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Improved Precision in Polyhedral Analysis with Wrapping
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0001-9341-4031
Mälardalen University, School of Innovation, Design and Engineering, Embedded Systems.ORCID iD: 0000-0001-5297-6548
Tidorum Ltd, Helsinki, Finland.
2017 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 133, p. 74-87Article in journal (Refereed) Published
Abstract [en]

Abstract interpretation using convex polyhedra is a common and powerful program analysis technique to discover linear relationships among variables in a program. However, the classical way of performing polyhedral analysis does not model the fact that values typically are stored as xed-size binary strings and usually have wrap-around semantics in the case of over ows. In resource-constrained embedded systems, where 8- or 16-bit processors are used, wrapping behaviour may even be used intentionally to save instructions and execution time. Thus, to analyse such systems accurately and correctly, the wrapping has to be modelled. We present an approach to polyhedral analysis which derives polyhedra that are bounded in all dimensions. Our approach is based on a previously suggested wrapping technique by Simon and King, combined with limited widening, a suitable placement of widening points and size-induced restrictions on unbounded variables. With this method, we can derive fully bounded polyhedra in every step of the analysis. We have implemented our method and Simon and King's method compared them. Our experiments show that for a suite of benchmark programs it gives at least as precise result as Simon and King's method. In some cases we obtain a significantly improved result.

Place, publisher, year, edition, pages
2017. Vol. 133, p. 74-87
National Category
Engineering and Technology Computer Systems
Identifiers
URN: urn:nbn:se:mdh:diva-17370DOI: 10.1016/j.scico.2016.07.006ISI: 000389391000004Scopus ID: 2-s2.0-84994454811OAI: oai:DiVA.org:mdh-17370DiVA, id: diva2:579701
Available from: 2012-12-20 Created: 2012-12-20 Last updated: 2019-06-26Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Bygde, StefanLisper, Björn

Search in DiVA

By author/editor
Bygde, StefanLisper, BjörnHolsti, Niklas
By organisation
Embedded Systems
In the same journal
Science of Computer Programming
Engineering and TechnologyComputer Systems

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 257 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf