Print Email Facebook Twitter Implementing the Decomposition of Soundness Proofs of Abstract Interpreters in Coq Title Implementing the Decomposition of Soundness Proofs of Abstract Interpreters in Coq Author de Waard, Jens (TU Delft Electrical Engineering, Mathematics and Computer Science) Contributor Visser, E. (mentor) Gousios, G. (graduation committee) Krebbers, R.J. (graduation committee) Keidel, S. (graduation committee) Degree granting institution Delft University of Technology Programme Computer Science Date 2021-02-03 Abstract Abstract interpretation is a way of approximating the semantics of a computer program, in which we derive properties of those programs without actually performing the necessary computations for running the program, through the use of an abstract interpreter. To be able to trust the result of the abstract interpretation, we would to able to prove the soundness of the approximations of the interpreter. Previous work by Keidel et al. has shown that the soundness proofs of an entire abstract interpreter can be simplified by decomposing the interpreter by implementing concrete and abstract interpreters as instantiations of a generic interpreter. The goal of this thesis is to explore and implement mechanical proofs of soundness of such interpreters. To this end, we have used the interactive proof assistant Coq to implement a generic interpeter for a simple imperative language and instantiate it both concrete and abstract versions. The abstract interpreter is automatically proven sound via the use of Coq's automatic proof capabilities and typeclass system. Both the interpreted language and the used abstractions can be expanded to allow for more features. Soundness proofs can then be written for just the new components, those proofs will then be automatically resolved by Coq. Subject CoqAbstract interpretationProof assistantsoundnessProof To reference this document use: http://resolver.tudelft.nl/uuid:54b01377-1f79-4758-b79b-4859df05dbd6 Part of collection Student theses Document type master thesis Rights © 2021 Jens de Waard Files PDF master_thesis_jens.pdf 216.46 KB Close viewer /islandora/object/uuid:54b01377-1f79-4758-b79b-4859df05dbd6/datastream/OBJ/view