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 metadatas

https://hal.inria.fr/hal-01110282
Contributor : Xavier Leroy <>
Submitted on : Tuesday, January 27, 2015 - 6:12:07 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM

Links full text

Identifiers

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. pp.107-116, ⟨10.1145/2103746.2103767⟩. ⟨hal-01110282⟩

Share

Metrics

Record views

82