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
Extension of the ELDARICA C model checker with heap memory
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2019 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

Model checking is a verification method which is used to detect bugs which would be extremely hard to detect using traditional testing, and ELDARICA is a state-of-the-art model checker which accepts a variety of formats as its input, including programs written in a fragment of the C language. This thesis aims to improve the C front-end of ELDARICA to a point where it can automatically model and verify C programs which contain pointers, heap memory interactions and structs, which are currently not supported. This work models the heap in a similar way to how it was done in JayHorn, a model checker for Java, by automatically finding quantified invariants which summarize the states of data structures that are on the heap. Support for structs is added by modeling them as algebraic data types, and limited support for stack pointers is added with some constraints on how they are declared and used. The initial experimental results are promising. The extended tool can now parse programs written in a larger fragment of the C language, with acceptable precision and performance in comparison to similar tools.

Place, publisher, year, edition, pages
2019. , p. 70
Series
IT ; 19078
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-397812OAI: oai:DiVA.org:uu-397812DiVA, id: diva2:1373067
Educational program
Masters Programme in Embedded Systems
Supervisors
Examiners
Available from: 2019-11-26 Created: 2019-11-26 Last updated: 2019-11-26Bibliographically approved

Open Access in DiVA

fulltext(861 kB)10 downloads
File information
File name FULLTEXT01.pdfFile size 861 kBChecksum SHA-512
d018d17f6262fe9a49f5227b8637bcc5ee83348b6952f956577e3a78f80623ea364036ab23fdad7890d732ccdb6f9029076034d4217d3dd0d79a19021d23e40d
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 10 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: 6 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