Software has become ubiquitous, ranging from apps for toasters to important infrastructure such as transportation, finance, and healthcare. Ensuring that software actually behaves as intended is critical in cases where implementation errors may lead to various forms of damage, such as financial losses, losses of private or confidential data, or even threats to human safety. To apply program verification to real-world programs a high degree of automation is vital. In this thesis, we expand the state-of-the-art in two areas where techniques for automated program verification remain challenging, namely the automated verification of modern logics with advanced correctness properties such as linearizability and the verification of language-agnostic information flow properties. Modern separation logics allow one to prove rich properties of intricate code, e.g. functional correctness and linearizability of non-blocking concurrent code. However, this expressiveness leads to a complexity that makes these logics difficult to apply. Manual proofs or proofs in interactive theorem provers consist of a large number of steps, often with subtle side conditions. On the other hand, automation with dedicated verifiers typically requires sophisticated proof search algorithms that are specific to the given program logic, resulting in limited tool support that makes it difficult to experiment with program logics, e.g. when learning, improving, or comparing them. In the context of secure information flow, security policies express the classification and declassification of data. Existing policy frameworks that support automated reasoning about code are tightly linked to a programming language, which limits their flexibility and complicates reasoning, for instance, during audits. Language-agnostic policy frameworks, which abstract the concrete behavior of programs, lack automated program verification. First, we present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations. We build our verification techniques for security properties on top of Gobra to apply them to a practical, real-world programming language. Second, we present a framework for the specification and verification of security policies for distributed systems, where attackers may observe the I/O performed by a program, but not its memory. Our policies are expressed over the I/O behaviors of programs and, thereby, language-agnostic. We present techniques to reason formally about policies, and to verify that an implementation satisfies a given policy. We formalize these verification techniques in Isabelle/HOL. An evaluation on several case studies, including an implementation of the WireGuard VPN key exchange protocol, demonstrates that our policies are expressive, and that verification is amenable to SMT-based verification. Third, we systematically develop a proof outline checker for the TaDA logic, a complex program logic for the verification of block-free code. Proof outline checkers take as input a program annotated with the most essential proof steps and then check automatically that this outline represents a valid proof in the program logic. Our proof outline checker reduces the verification of the TaDA logic to a simpler verification problem, for which automated tools exist. Our approach leads to proof outline checkers that provide substantially more automation than interactive provers, but are much simpler to develop than custom automatic verifiers.