Artifact and Appendix of "RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types"

Abstract

This is the artifact for the PLDI'21 paper "RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types". It contains the RefinedC tool including its Coq development and the appendix for the paper. Copyright: Creative Commons Attribution 4.0 International Open Access