Automatic software verification traditionally relies on over-approximations of program behaviour to guarantee that no trace violates a specified property. However, such over-approximations may lead to false positives, which are particularly undesirable in non-critical environments. In contrast, under-approximating approaches, while potentially missing some errors, are more appealing when strong correctness guarantees are not strictly required, as they ensure that every detected violation is a true error (at the cost of possibly failing to detect others). This thesis presents a framework for backward under-approximating static analysis based on abstract interpretation. The approach computes sufficient preconditions and can be applied, for instance, to derive liberal preconditions for runtime errors or to infer code contracts for program correctness. The method is both complete and fully automatic. The contributions of this work are twofold. First, we extend the semantic model and abstract domains to support the analysis of realistic C-like languages. This includes the introduction of under-approximating operators for abstract domains (such as intervals, polyhedra, and powerset constructions) and extensions to the language semantics to support integer variable wrapping and input statements. To enable memory-aware reasoning, we extend both the language and its semantics to account for low-level memory access (i.e., via pointers) and dynamic memory allocations and deallocations. This is achieved through the development of a backward concrete semantics and an abstraction based on the cell domain and heap-recency abstraction. Second, these theoretical advances are integrated into the MOPSA static analyzer, where the backward under-approximating analysis is integrated into the analyzer supporting both numeric and memory reasoning. We briefly describe the modifications required in the analyzer, such as extensions to domain signatures and updates to expression evaluation mechanisms, and present an experimental evaluation of both precision and performance. The tool was evaluated through participation in the Software Verification Competition (SV-COMP), where it demonstrated good precision in the MemSafety and NoOverflows categories, successfully analyzing 45% of the tasks. However, precision was lower in the ReachSafety and SoftwareSystems categories, due to the increased complexity of the properties being verified and the larger scale of the programs involved. While our analyzer is generally less precise than state-of-the-art tools, it requires fewer computational resources: on average, other tools consume between 38% and 220% more time. Overall, this work extends abstract interpretation techniques for the inference of sufficient preconditions from a theoretical foundation to a practical, applicable method suitable for real-world programming languages.