Program verification constantly navigates a fundamental tension: we want analyses that are both sound (no bugs are missed) and precise (no false alarms are reported). Abstract interpretation provides a general and powerful framework for sound static analysis, yet precision is often elusive: non-trivial abstractions are inherently incomplete, and even correct programs can easily trigger spurious warnings. This course explores the notion of precision in program verification through the lens of abstract interpretation. We will examine why perfect precision (i.e., "global completeness") is often unrealistic in practice, and how even minor changes in program structure can significantly influence the outcome of an analysis. These limitations motivate weaker but more practical notions, such as local completeness, which enable more refined reasoning about specific inputs and execution paths. Building on these ideas, we will present logical systems that combine reasoning about correctness ("nothing bad happens") with reasoning about incorrectness ("this bug is real") within a unified conceptual framework. We will also discuss domain refinement techniques that dynamically enhance precision by eliminating false alarms only where necessary. By bridging foundational theory and recent advances in program logics and verification techniques, the course addresses a central question: how precise can program verification truly be?