A Deflate-like compressor in HOL, Creating executable binaries using CakeML
Typ
Examensarbete för masterexamen
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2022
Författare
Carlsson, Eric
Rönning, Li
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
Deflate 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.
Beskrivning
Ämne/nyckelord
Deflate , Huffman encoding , LZSS compression , formal verification , interactive theorem prover , HOL , CakeML