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 (static and dynamic) contract checker for a subset of OCaml. The key technique is symbolic simplification, which makes integrating static and dynamic contract checking easy and effective. Our technique statically checks contract satisfaction or blames the function violating the contract. When a contract satisfaction is undecidable, it leaves residual code for dynamic contract checking.
Type de document :
Communication dans un congrès
PEPM'12: ACM workshop on Partial evaluation and program manipulation, Jan 2012, Philadelphia, United States. ACM, pp.107-116, 〈10.1145/2103746.2103767〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01110282
Contributeur : Xavier Leroy <>
Soumis le : mardi 27 janvier 2015 - 18:12:07
Dernière modification le : vendredi 25 mai 2018 - 12:02:07

Lien texte intégral

Identifiants

Collections

Citation

Dana N. Xu. Hybrid contract checking via symbolic simplification. PEPM'12: ACM workshop on Partial evaluation and program manipulation, Jan 2012, Philadelphia, United States. ACM, pp.107-116, 〈10.1145/2103746.2103767〉. 〈hal-01110282〉

Partager

Métriques

Consultations de la notice

51