HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

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
Complete list of metadata

https://hal.inria.fr/hal-00644156
Contributor : Na Xu Connect in order to contact the contributor
Submitted on : Wednesday, November 23, 2011 - 4:51:56 PM
Last modification on : Thursday, February 3, 2022 - 11:13:55 AM
Long-term archiving on: : 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

87

Files downloads

81