This text is a self-contained introduction to program verification using logic-based methods, presented in the broader context of formal methods for software engineering. It focuses on two approaches: the Coq proof assistant and the B suite.