ABSTRACT. Proof by coupling is a classical technique for proving properties about pairs of randomized algorithms by carefully relating (or coupling) two probabilistic executions. In this paper, our goal is to automatically construct such proofs for programs. First, we present f-coupled postconditions, an abstraction describing two coupled programs. Second, we show how specific forms of f-coupled postconditions imply probabilistic properties like uniformity and independence of program variables. Third, we demonstrate how to automate construction of coupling proofs by reducing the problem to solving a purely logical synthesis problem of the form ∃f. ∀X. φ, thus doing away with probabilistic reasoning. Finally, we evaluate our technique in a prototype implementation, and demonstrate its ability to construct a range of coupling proofs for various properties and randomized algorithms.