A smart contract is a program whose current state and source code are stored on a blockchain-based platform. They have the potential of facilitating legal, financial, and social agreements. Correctness and efficiency are crucial properties of smart contracts because, among other things, they are immutable after deployment, they are valuable (in the corresponding blockchain cryptocurrency), and handle key information (e.g., DeFi applications). Hence software bugs and inefficiencies can cause economic (sometimes irreversible) losses. This talk will give an overview of various applications of program analysis techniques in the context of the optimization and verification of (Ethereum) smart contracts and the tools we have developed.