Hybrid Contract Checking via Symbolic Simplification

Abstract : Program errors are hard to detect or prove absent. Allowing programmers to write formal and precise specifications, especially in the form of contracts, is a popular approach to program verification and error discovery. We formalize and implement a hybrid contract checker, that is static checking followed by dynamic checking, for a subset of OCaml. The key technique we use is symbolic simplification, which makes integrating static and dynamic contract checking easy and effective. Our technique statically verifies that a function either satisfies its contract or blames the function violating the contract. When a contract satisfaction is undecidable, it leaves residual code for dynamic contract checking.
Type de document :
Rapport
[Research Report] RR-7794, INRIA. 2011
Liste complète des métadonnées

https://hal.inria.fr/hal-00644156
Contributeur : Na Xu <>
Soumis le : mercredi 23 novembre 2011 - 16:51:56
Dernière modification le : vendredi 25 mai 2018 - 12:02:07
Document(s) archivé(s) le : vendredi 24 février 2012 - 02:31:01

Fichier

RR-7794.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00644156, version 1

Collections

Citation

Na Xu. Hybrid Contract Checking via Symbolic Simplification. [Research Report] RR-7794, INRIA. 2011. 〈hal-00644156〉

Partager

Métriques

Consultations de la notice

173

Téléchargements de fichiers

82