Embracing a mechanized formalization gap
Programming Languages
2019-10-28 v1
Abstract
If a code base is so big and complicated that complete mechanical verification is intractable, can we still apply and benefit from verification methods? We show that by allowing a deliberate mechanized formalization gap we can shrink and simplify the model until it is manageable, while still retaining a meaningful, declaratively documented connection to the original, unmodified source code. Concretely, we translate core parts of the Haskell compiler GHC into Coq, using hs-to-coq, and verify invariants related to the use of term variables.
Cite
@article{arxiv.1910.11724,
title = {Embracing a mechanized formalization gap},
author = {Antal Spector-Zabusky and Joachim Breitner and Yao Li and Stephanie Weirich},
journal= {arXiv preprint arXiv:1910.11724},
year = {2019}
}
Comments
Submitted to CPP'20