A Deflate-like compressor in HOL, Creating executable binaries using CakeML

Visa enkel post
dc.contributor.authorCarlsson, Eric
dc.contributor.authorRönning, Li
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data och informationstekniksv
dc.contributor.examinerSeger, Carl-Johan
dc.contributor.supervisorMyreen, Magnus
dc.date.accessioned2022-09-20T09:23:28Z
dc.date.available2022-09-20T09:23:28Z
dc.date.issued2022sv
dc.date.submitted2020
dc.description.abstractDeflate is a well-known file format specification of lossless compression, with implementations in software like gzip and zip. Proving that a compressor following the Deflate algorithm has the property of being entirely reversible is of interest, as Deflate is widely used. The aim of this project is to produce verified binaries for the Deflate algorithm using the interactive theorem prover HOL4 and the CakeML compiler. The implementation consists of three main parts: the LZSS compression algorithm, the Huffman encoding algorithm, and the Deflate algorithm. Since the focus was to properly implement Deflate, the majority of our effort was put into developing the algorithm itself. Due to time constraints however, our implementation reached an executable implementation of a Deflate-like algorithm. While the Deflate algorithm has been implemented and verified before, the work described here is the first to produce an executable binary of a compression specification.sv
dc.identifier.coursecodeDATX05sv
dc.identifier.urihttps://hdl.handle.net/20.500.12380/305628
dc.language.isoengsv
dc.setspec.uppsokTechnology
dc.subjectDeflatesv
dc.subjectHuffman encodingsv
dc.subjectLZSS compressionsv
dc.subjectformal verificationsv
dc.subjectinteractive theorem proversv
dc.subjectHOLsv
dc.subjectCakeMLsv
dc.titleA Deflate-like compressor in HOL, Creating executable binaries using CakeMLsv
dc.type.degreeExamensarbete för masterexamensv
dc.type.uppsokH
local.programmeComputer science – algorithms, languages and logic (MPALG), MSc
Ladda ner
Original bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
CSE 22-64 Carlsson Rönning.pdf
Storlek:
1.29 MB
Format:
Adobe Portable Document Format
Beskrivning:
A Deflate-like compressor in HOL
Ladda ner
License bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
license.txt
Storlek:
1.51 KB
Format:
Item-specific license agreed upon to submission
Beskrivning:
Ladda ner
Samling
Examensarbeten för masterexamen