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
Abstract Interpretation of Unstructured Imperative Languages on Unbounded Domains
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2011 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

In this thesis we present a novel program analysis technique that applies abstract interpretation to low-level intermediate languages with unbounded abstract domains. Unbounded abstract domains in program analysis occur in applications such as finding ranges of variables and its applications include elimination of assertions in programs, automatically deducing numerical stability, and array bounds checking. Unbounded abstract domains impose a major challenge in program analysis because it is difficult to ensure the termination of the analysis in the presence of program cycles. State-of-the-art methods propose a technique that relies on a structured composition of programs, e.g., they permit abstract interpretation with unbounded abstract domains for program languages that have while and if statements but do not have goto statements.

This work demonstrates that unbounded abstract domains can be employed in program analysis for low-level intermediate languages commonly used in program language tools including compilers, integrated-development environments, and bug-checkers, where loops are implicit within the control flow graph.

Our work combines methods of elimination-based data flow analysis with abstract interpretation. We have implemented the proposed framework in the LLVM compiler framework as a program analysis pass and have conducted experiments with a suite of test programs to show the feasibility of our approach.

Place, publisher, year, edition, pages
2011.
Series
IT, 11 044
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-159034OAI: oai:DiVA.org:uu-159034DiVA: diva2:442326
Educational program
Master Programme in Computer Science
Uppsok
Technology
Supervisors
Examiners
Available from: 2011-09-21 Created: 2011-09-21 Last updated: 2011-09-21Bibliographically approved

Open Access in DiVA

fulltext(868 kB)417 downloads
File information
File name FULLTEXT01.pdfFile size 868 kBChecksum SHA-512
bc1b1cc0d6503c9ad6dc96844bcf8da54a470a207b3e4a79ac56c41cd0a6e33afb29e3edfdc6b5401ebb7f1ba782fed62838dd6ec161900a89678a62f5d46687
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 417 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 458 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