ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Thu 15 Sep 2022 16:40 - 17:00 at Štih - Verification Chair(s): Stephen Dolan

The formal, mechanized, verification of computer programs is a particularly difficult task in fast-evolving and complex development environments, as it typically is a slow process. To speed this effort up, verification efforts often target abstract models of these programs, and many implementation details are often left unverified in critical code. In this work, we propose to bridge the verification gap between a mechanized model and its implementation by leveraging property-based testing. Concretely, we present a light-weight automated tool for extracting F* specifications as OCaml predicates for its execution as a QCheck tests.

Verify, but test: extracting property-based tests from F* specifications (ml2022-paper96.pdf)433KiB

Thu 15 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change