University of Twente Student Theses
Verified Parser- and Printer-Combinator Bidefinition in the Isabelle Proof Assistant
Sleurink, Matthias (2024) Verified Parser- and Printer-Combinator Bidefinition in the Isabelle Proof Assistant.
|
PDF
1MB |
| Abstract: | Parsers and printers are commonly used to transfer data, for example, using the JSON or XML formats. The correctness of these parsers and printers is pertinent to the functioning of the systems that use them to communicate. The separate design and programming of parsers and printers can cause slight differences in behaviour over time due to programming mistakes. By programming the parser and printer simultaneously, using the same expression, we can be sure their behaviours never deviate. Software verification is the practice of verifying the correctness of software. If a piece of software is verified, the verifier might need to verify the parsers and printers in the software as well. In this work, we introduce both a parser and printer bidefinition-combinator library and systems to verify that the bidefinitions created with it are compatible, created in the Isabelle proof assistant. To define what compatible behaviour means, we will describe various efforts made in the past to determine this and explain our choice of definition. |
| Item Type: | Essay (Master) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/104408 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page