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.

Smart contracts are programs that reside and execute on top of blockchains. These programs commonly perform financial transactions and contain the backend logic of various blockchain-supported applications. The presence of errors and bugs in smart contracts poses security risks to the applications they support. This is especially concerning because operations performed by smart contracts are irreversible by design, which is a key feature enforced by blockchain technology. Thus, ensuring the correctness and security of smart contracts before deployment is crucial. To achieve this, 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 stateof-the-art. The first contribution of this thesis is an investigation into how predeployment analysis techniques have been applied to 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 issues uncovered by the investigation, one notable set pertains to nondeterministic (ND) factors involved in smart contract execution in the Ethereum blockchain. For example, transactions (function invocations) dispatched to Ethereum smart contracts are scheduled in ND order, and inputs received during execution, such as inputs from asynchronous callbacks of Oracles and externally called contracts that halt unexpectedly, are nondeterministic. Consequently, these factors may cause risks of ND changes to the state of smart contracts. The second contribution of this thesis is the proposal of methods for the static (at pre-deployment) detection of program sites (for example, state variables or cryptocurrency transfer instructions) susceptible to ND changes due to ND transaction scheduling or ND inputs and return values (from asynchronous callbacks and externally called contracts) in Ethereum smart contracts. The evaluations show that our approaches can outperform existing methods with respect to efficacy and runtime