Confiance, Preuve et Probabilités – CPP

In the context of proofs of safety properties for critical software, The CPP project proposes to study the joint use of probabilistic and formal (deterministic) methods, in a way to improve the applicability and precision of static analysis methods on numerical programs. Partners will first construct a solid demonstration case of the usefulness of the project by extracting some relevant piece of industrial code provided by Hispano-Suiza, and produce results using current state of the art methods (basic Monte-Carlo simulations for instance). These results will be matched against the new results at the end of the project, as a (partial) assessment of our methods. Then, partners will lay the theoretical foundations of the analysis techniques developped in the project. Based on existing expertise of some of the partners of the project in belief functions and prevision semantics, we will derive new probabilistic/deterministic semantics for numerical programs After that, we will need to find good (computable) approximation schemes of the semantics defined earlier. We already think of generalisations of P-boxes in particular. We also want to combine this approach with hybrid systems approaches, when partial deterministic information (finer than interval ranges, for instance, systems of ODEs) is available on the external environment. A very important application area is that of characterizing the precision of calculations of the numerical program that we wish to analyse, and some experiments will be conducted in the FLUCTUAT project. We also plan to refine our view of numerical computations in the presence of data or parametric uncertainties, as well as computational imprecision. Our view is that we cannot disqualify a code which does not have the same "real number" and "floating-point number" control flow for instance, as they might end up with very similar results. Bisimulation distance is one way we envision, will enlighten our understanding of the numerical quality of codes.