There exists a large spectrum of techniques for proving correctness of computer programs. At one end is the Curry-Howard isomorphism, in which a typing procedure automatically checks the correctness of a program, and at the other end are techniques à la Hoare, in which non-trivial reasonning is performed in a logic adapted to the programming language. Realizability can be seen as a mixture of these two approaches: proving that a program realizes a specification is done via a combination of automatic techniques in a Curry-Howard fashion, and manual proofs of correctness of subprograms with respect to some axioms. In my talk I will present some realizability models where the realizability relation is defined semantically: a program realizes a specification if its denotation satisfies a property in the model. The denotational models involved include game semantics, continuation models and Scott domains.