Recherche de bornes maximales pour la vérification de programmes
14/12/10 10:14 | Stages 2010/11
Laboratoire : I3S
Equipe : CeP
Contact : Michel Rueher (michel point rueher arobase unice point fr)

La vérification automatique de programmes est reconnue comme l’un des grands challenges de la recherche en informatique. Deux techniques complémentaires sont aujourd'hui utilisées: l'interprétation abstraite et la vérification de modèle bornée (Bounded Model Checking).

Les outils basés sur l'interprétation abstraite[1] construisent une approximation des programmes et permettent de garantir qu'un programme ne vas pas provoquer des erreurs d'exécution suite à une division par 0, au dépassement des bornes d'un tableau, ou suite à un débordement sur les entiers.

Les techniques de Bounded Model Checking (BMC) permettent de vérifier des propriétés plus complexes mais la violation de ces propriétés n'est détectée que pour des bornes fixées. Les techniques de BMC ont été largement utilisées dans l'industrie des semi-conducteurs pour trouver des erreurs dans la conception de matériel et sont de plus en plus utilisées pour les logiciels [2]. Le processus de vérification (cf. [3]) consiste principalement à:

  • Dérouler le programme k fois,
  • Traduire le programme et la propriété en une formule F telle que F est satisfiable si et seulement si il existe un contre-exemple de profondeur inférieure à k
  • Utiliser un solveur pour vérifier la satisfiabilité de F. L'utilisation des techniques de programmation par contraintes dans cette dernière étape permet de fournir un contre-exemple lorsque la formule n'est pas vérifiée [4,5].

Le problème qu'on propose de traiter ici concerne la recherche des valeurs maximales des données d'entrée pour qu'un programme soit correct, c'est à dire pour qu'un outil d'interprétation abstraite puisse garantir qu'il n'y a pas de débordement et qu'un outil de BMC puisse vérifier certaines propriétés. Dans le cadre de ce projet on abordera ce problème avec les techniques de programmation par contraintes et on se restreindra aux entiers.


[1] The ASTRÉE Static Analyzer. http://www.astree.ens.fr/
[2] Vijay D'Silva, Daniel Kroening, and Georg Weissenbacher. A survey of automated techniques for formal software verifcation. IEEE Trans. on CAD of Integrated Circuits and Systems, 27(7):1165-1178, 2008.
[3] Malay K Ganai and Aarti Gupta. Accelerating high-level bounded model checking. In ICCAD, pages 794- 801. ACM, 2006.
[4] A Constraint-Programming Framework for Bounded Program Verification. Hélène Collavizza, Michel Rueher, and Pascal Van Hentenryck. Constraints Journal, Springer Verlag, vol. 15(2):238-264, 2010.
[5] Exploration of the capabilities of Constraint Programming Techniques for Software Verification . Hélène Collavizza and Michel Rueher.Proceedings of TACAS 06 (TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, LNCS: 3920/2006:182-196, 2006.
[6] CBMC : a Bounded Model Checker for ANSI-C and C++ programs. http://www.cprover.org/cbmc/