Static analysis is a widespread method to gain confidence in the reliability of software. Such analyses are mainly carried out on source code but Reps et al. highlight the relevance of analysing executables because of what they call the WYSINWYX phenomenon. They have therefore designed the value-set analysis and implemented it in CodeSurfer/x86, their tool for analysing x86 executables. However executables may be obfuscated, i.e. made hard to analyse. Although there are specific desobfuscation methods to address the analysis of obfuscated programs, we wonder how robust generic analyses and tools are, and up to which extent they are able to yield sound and precise results. The case of soundness is also addressed from an other point of view: in order to trust an analysis result, there must be strong evidence that the analyser is correct. Formal methods can provide such evidence. In this study we first review obfuscation purposes and techniques, as well as the method of the value-set analysis. Then experiments are carried on to better understand the robustness of analysers. Finally thanks to the Coq proof assistant, a subset of the value-set analysis for a toy assembly-like language is formalized. A certified checker enables to prove the soundness of a result.