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