Smart contracts are programs that reside and execute on top of blockchains. These programs commonly perform financial transactions and contain the backend logic of several blockchain-supported applications. The presence of errors and bugs in smart contracts poses security threats to the applications they support. This is especially concerning because operations performed by smart contracts are irreversible after deployment due to the immutable nature of blockchains. Thus, ensuring their correctness and security before deployment is important. For this purpose, several program analysis and verification approaches are being actively researched and applied to smart contracts.

The volume of research in this area makes it challenging to articulate the state-of-the-art. The first contribution of this thesis is to investigate how predeployment analysis techniques ensure the correctness and security of smart contracts. This investigation factors out the relationship between vulnerabilities in smart contracts and pre-deployment analysis techniques through properties they address.

Among the range of issues uncovered by the investigation, one notable set pertains to non-deterministic factors involved in the context of contract execution. For example, transactions (function invocations) dispatched to smart contracts are scheduled in non-deterministic order, and asynchronous calls to external services (known as oracles) return in a non-deterministic order. Consequently, these factors may cause data races and non-deterministic bugs in smart contracts. The second contribution of this thesis is to address such issues by unraveling specific forms of data races in Ethereum smart contracts, denoted as transactional data races. The thesis also presents a static analysis approach to detect issues arising from transactional data races.

In addition, this thesis makes a third contribution relating to a design approach for Domain Specific Languages (DSLs). Research on DSL design approaches has the potential to complement the research on smart contracts, as smart contracts are commonly written using DSLs. This thesis proposes an agile approach for designing a DSL for automotive safety test grounds. This approach enables increased communication and learning between different stakeholders involved in DSL development.

Finally, this thesis highlights our future research endeavors concerning various forms of concurrency and non-determinism-related issues in smart contracts.