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.
Document type :
Reports
[Research Report] RR-7794, INRIA. 2011
Liste complète des métadonnées

https://hal.inria.fr/hal-00644156
Contributor : Na Xu <>
Submitted on : Wednesday, November 23, 2011 - 4:51:56 PM
Last modification on : Saturday, September 17, 2016 - 1:37:28 AM
Document(s) archivé(s) le : Friday, February 24, 2012 - 2:31:01 AM

File

RR-7794.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00644156, version 1

Collections

Citation

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

Share

Metrics

Record views

135

Document downloads

70