dc.rights.license | CC-BY-NC-ND | |
dc.contributor.advisor | Hage, J. | |
dc.contributor.advisor | Swierstra, W.S. | |
dc.contributor.author | Wijk, J.J. van | |
dc.date.accessioned | 2017-07-26T17:01:31Z | |
dc.date.available | 2017-07-26T17:01:31Z | |
dc.date.issued | 2017 | |
dc.identifier.uri | https://studenttheses.uu.nl/handle/20.500.12932/26361 | |
dc.description.abstract | Compiler builders use monotone frameworks to perform static analysis. Often,
they omit proof of the domain of the function being a bounded semi lattice or only
argue why their domain should be.
Unfortunately, mistakes in their argumentation could result in a non terminat-
ing static analysis. Since important software, such as compilers, often depends on
the results of a static analysis, embedding a non terminating analysis causes such
software to loop.
To assist programmers in their reasoning and to obtain machine verified proofs
of termination, this thesis presents a verified implementation of embellished, ex-
tended and regular monotone frameworks in Agda. The implementation contains
several algorithms to compute the least fixed point of a function that represents
the flow of information for the static analysis on an input program. That program is
written in a simplified procedural programming language.
To facilitate construction of termination proofs, we introduce a set of bounded
semi lattice combinators which can be used to compose the domain of a transfer
function. The bounded semi lattice constructed by the combinators includes a proof
that the partial order is conversely well founded and thus implies the ascending
chain condition.
Finally, we perform classical analyses on a intra-procedural and inter-procedural
language. | |
dc.description.sponsorship | Utrecht University | |
dc.format.extent | 246946 | |
dc.format.mimetype | application/pdf | |
dc.language.iso | en | |
dc.title | Formalising Monotone Frameworks: A dependently typed implementation in Agda | |
dc.type.content | Master Thesis | |
dc.rights.accessrights | Open Access | |
dc.subject.keywords | monotone frameworks, agda, static analysis, fixed point computation, extended monotone frameworks, embellished monotone frameworks | |
dc.subject.courseuu | Computing Science | |