Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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
Extraction of Rust code from the Why3 verification platform
Luleå University of Technology, Department of Computer Science, Electrical and Space Engineering.
2019 (English)Independent thesis Advanced level (degree of Master (Two Years)), 180 HE creditsStudent thesis
Abstract [en]

It is hard to ensure correctness as software grows more complex. There are many ways to tackle this problem. Improved documentation can prevent misunderstandings what an interface does. Well built abstractions can prevent some kinds of misuse. Tests can find errors, but unless they are exhaustive, they can never guarantee the absence of errors. The use of formal methods can improve the reliability of software. This work uses the Why3 program verification platform to produce Rust code. Possible semantic-preserving mappings from WhyML to Rust are evaluated, and a subset of the mappings are automated using Why3's extraction framework.

Place, publisher, year, edition, pages
2019.
Keywords [en]
Formal verification
National Category
Computer Sciences Engineering and Technology
Identifiers
URN: urn:nbn:se:ltu:diva-73510OAI: oai:DiVA.org:ltu-73510DiVA, id: diva2:1303268
Subject / course
Student thesis, at least 30 credits
Educational program
Computer Science and Engineering, master's level
Supervisors
Examiners
Available from: 2019-04-10 Created: 2019-04-09 Last updated: 2019-04-10Bibliographically approved

Open Access in DiVA

fulltext(1049 kB)31 downloads
File information
File name FULLTEXT02.pdfFile size 1049 kBChecksum SHA-512
2cea4af7dc7a10f5f3a7d49fe65b839b0760fc54dfe3d8a70c63d5f5655cb9adddf48fcd89e14874090beb90b5bb7306a17c421e9465587cb067df05360fbd0c
Type fulltextMimetype application/pdf

By organisation
Department of Computer Science, Electrical and Space Engineering
Computer SciencesEngineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 31 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: 65 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • 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