Since software systems increasingly govern both vital infrastructure and people's daily lives, ensuring their safety and security is vital. Where standard measures like testing are insufficient, deductive verification can be used to mathematically prove software properties once and for all. In the past decades, there has been huge progress in the design and automation of verification techniques, to the point where there are multiple automated verification tools able to prove trace properties for statically-typed programming languages like Java or C. However, several challenges remain: Crucial security properties like non-interference are hyperproperties, which are not supported by most standard verification tools. Additionally, new verification techniques have to be developed to enable the verification of programs written in other mainstream programming languages that offer fewer or different static guarantees. In this thesis, we expand the state of the art in these two directions, by enabling the automated verification of hyperproperties in standard verification tools, and making existing verification techniques accessible for the dynamic Python language as well as Ethereum smart contracts. First, we present a modular verification for Python programs, targeting complex safety and security properties for realistic code. We address the challenges stemming from dynamic typing and the resulting lack of static knowledge about Python programs using a mix of permissive static checks using an unsound type system and additional sound checks in the verifier. The resulting verification technique is able to support typical Python code patterns, and can be integrated with existing specification and verification techniques for safety and security properties. We implement our solution in Nagini, an automated verifier for a substantial subset of Python 3, and demonstrate its ability to verify real-world Python code and prove complex program properties. Second, we present modular product programs, a program transformation that enables the verification of hyperproperties using standard verification tools. Unlike existing solutions, modular product programs can be constructed automatically, impose no restrictions on program control flow, and, crucially, enable modular proofs of hyperproperties using relational specifications. We apply modular product programs to proving non-interference using special information flow specifications, which can express complex properties like value-dependent sensitivity and termination-sensitive non-interference. We implement the product transformation for the Viper verification infrastructure and show that it can prove both information flow properties and other hyperproperties for challenging examples from the literature. Third, we show how product constructions like the aforementioned modular product programs, which are usually defined for small, sequential languages, can be applied to more complex languages and integrated with existing verification tools that are based on intermediate verification languages (IVLs). The key idea is to perform the product construction on the level of the (simple) IVL instead of the (complex) source language, thus enabling existing tools to verify hyperproperties with little engineering effort. We show that this approach is not always sound, but provide a simple criterion that guarantees soundness and can be easily checked in practice. Furthermore, we show how one can verify non-interference properties of concurrent source programs using sequential product constructions. We demonstrate the feasibility of this approach by implementing it for Nagini. Our evaluation shows that this extended Nagini implementation …