Scilex-3 From high-level to low-level certification

Many techniques are known today to certify programs: refinement, theorem proving, model-checking, static analysis, testing, and so on. None is enough in isolation to verify large pieces of software, from specification to machine code. Moreover, each technique has its own strengths and weaknesses, but cooperation between existing tools and with tools of different natures is limited.

Currently, verification is done at each stage of the development. This involves useless repetition of tasks at various abstraction levels (specification, model, source code, machine code), using different techniques and tools.

One way to combine verification techniques is to implement them inside the same logical framework: proof assistants such as Coq and Isabelle/HOL have been successfully used as environments to support tools for program analysis, including abstract interpreters, model checkers, test case generators. However, because they are interactive and based on a general mathematical language, these tools require a great sum of expertise before being able to address real-life problems. The next step is to move towards program verification platforms (for example Why-3 or Frama-C) to handle the computer memory model more directly and to use recent advances in automated deduction (especially SMT solvers).

Hot topics