Combining over and underapproximation of memory abstractions for low-level code analysis

Job description: Riceapos;s theorem stating that no method can automatically tell whether a property of a program is true or not has led to the separation of verification tools into two groups: sound tools operating by over-approximation, such as abstract interpretation, are able to automatically prove that certain properties are true, but are sometimes unable to conclude and produce alarms; conversely, complete tools operating by under-approximation, such as symbolic execution, are able to produce counter-examples, but are unable to demonstrate whether a property is true. *The general aim of the thesis is to study the combination of sound and complete methods of programanalysis, and in particular static analysis by abstract interpretation and the generation of underapproximated formulae by symbolic execution*. We are particularly interested in the combination of over- and sub-approximating abstractions, especially for memory. The priority applications envisaged concern the analysis of code at the binary level, as achieved by the combination of the BINSEC and CODEX analysis platforms, so as to automatically discover new security vulnerabilities, or prove their absence.