Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Tuesday, January 27, 2015 - 6:12:07 PM
Last modification on : Thursday, February 3, 2022 - 11:18:57 AM

Links full text




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



Record views