The Move programming language, designed with strong safety guarantees such as linear resource semantics and borrow-checking, has emerged as a secure and reliable choice for writing smart contracts. However, these guarantees depend on the assumption that all interacting contracts are well-formed—a condition naturally met in Move's native execution environment but not in heterogeneous or untrusted platforms like the Ethereum Virtual Machine (EVM). This hinders the usage of Move as a source language for such platforms: for instance, we show in this paper that the existing Move-to-EVM compiler is not secure, meaning the compilation of secure Move contracts yields vulnerable EVM bytecode.This work addresses the challenge of preserving Move's security guarantees when compiling to EVM. We introduce a novel compiler design extending the existing Move-to-EVM compiler with an Inlined-Reference-Monitor-(IRM)-based protection layer. Our approach enforces Move's linear semantics and borrow-checking rules at runtime in EVM, ensuring the correctness and safety of the compiled smart contracts, even in adversarial execution environments. We formally define the compilation process, establish correctness guarantees for the translation, and implement our protection mechanism in the original compiler. Our evaluation draws on three datasets: (i) an ERC-20 implementation in Solidity and Move, (ii) the Rosetta dataset curated by Bartoletti et al., and (iii) modules scraped from the Aptos blockchain. The performance evaluation shows that the gas cost overhead introduced by our compiler—compared both to the original compiler and Solidity-compiled code—is modest, thereby confirming our approach as a practical solution for bringing the security guarantees of Move code to the EVM.

Proving arithmetic properties has many applications, ranging from classical use cases of computer algebra and functional analysis to more applied case studies from software analysis and verification. For example, program loops over numeric data structures naturally implement addition, multiplication and exponentiation operations. While automating reasoning about such arithmetic properties has already made significant progress in the domain of linear algebra, non-linear reasoning in the context of satisfiability and validity checking is sill at its infancy. Although this subfield of automated reasoning is still quite unexplored, there do exist SMT-solvers (satisfiability modulo theory) which are able to reason about such non-linear arithmetic properties. Whenever new proving techniques or improvements are discovered, a typical approach to evaluate their performance is to test them on challenges of varying difficulty and compare different metrics like runtime or quality of the result (e.g. length of the proof) with those of other solvers. For non-linear arithmetic over reals and over integers, a large dataset of such challenges already exists (e.g. SMT-Lib benchmarks). Although these benchmarks are well suited for performance tests, they are often complex and only theoretically readable by humans. Therefore, it usually becomes difficult to get to the real problem when a benchmark is not solved. In this thesis, we describe various ways to generate benchmarks where the complexitycan be adjusted in different ways. The benchmarks are not created from scratch but are based on challenges originally designed for loop invariant generators. For a wide range of loops, these invariants can be represented by polynomials over the variables occurring in the program, which makes them a perfect fit for our benchmarks. The benchmarks formulate a correctness claim for polynomial loop invariants in first-order logic. All the methods described in this thesis for generating such benchmarks are proven to be sound. That is, we show that the correctness claim is a valid formula if and only if the corresponding polynomial invariant is indeed an invariant of the considered loop. The already mentioned variation of the benchmark is then achieved by exploiting properties of polynomial invariants. Experiments on the generated benchmarks were then conducted, using the two state-of-the-art solvers Vampire and Z3. Based on the resultsof the experiments, we have investigated the impact of varying the complexity of the benchmarks. Additionally, we suggest further approaches and adaptions to the solver in an attempt to improve their performance