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.

Many program transformation languages simplify the implementation of program transformations. However, they give only weak static guarantees about the generated code such as well-sortedness. Well-sortedness guarantees that a program transformation does not generate syntactically ill-formed code, but it is too imprecise for many other scenarios. In this paper, we present a static analysis that allows developers of program transformations to reason about their transformations on a more fine-grained level, namely that of syntactic shape. Specifically, we present an abstract interpreter for the Stratego program transformation language that approximates the syntactic shape of transformed code using regular tree grammars. As a baseline, we also present an abstract interpreter that guarantees well-sortedness. We prove parts of both abstract interpreters sound.

Null pointer dereferences in Java raise exceptions, occur often, are hard to debug and cost a lot of unnecessary effort and resources. Therefore, a lot of effort has been put in analyses spotting those null pointer dereferences. As developers rely on those analyses it is important that they are sound. However, proving null pointer analyses sound has been a complex problem. Hence, we developed a nullness analysis for Java that is provably sound. The analysis is built as an abstract interpreter upon the sturdy framework, that allows for compositional soundness proofs. This reduces the proof effort greatly. By creating a concrete interpreter, and by generating arbitrary programs, we were able to assess the soundness of the nullness analysis to great extend. Also, we have proven a part of the analysis to be sound in a formal way.

Since its inception in 1995, JavaScript usage has grown far beyond its initial domain of interactive websites. As the size of applications developed in the language grows, so does the desire for static analysis such as typechecking to provide safety and reliability. Many developments have been made in recent years on increasing the precision of analysis of JavaScript. This work introduces a concrete and a type interpreter for LambdaJS implemented within the Sturdy framework. The goal of this work is to evaluate the feasibility of implementing a shared interpreter using the Sturdy framework, evaluate the correctness of the concrete interpreter, and evaluate the feasibility of proving the typechecker sound. The resulting interpreters are tested experimentally with two test suites. The experimental evaluation gives confidence in the correctness of the concrete and abstract interpreter. A small part of the abstract interpreter is proven sound to evaluate the difficultyofcreatingacompletesoundnessproof.Thesuccessful implementation of the interpreters shows that implementing a shared arrow-based interpreter within the Sturdy framework is feasible for languages with complex semantics, that the utilities available reduce the effort required to do so, and that proving the abstract interpreter sound is simplified by using the library.