Artifact and Appendix of "VIP: Verifying Real-World C Idioms with Integer-Pointer Casts"

integration_instructionsResearch softwarekeyboard_double_arrow_right Software 09 Nov 2021 English Publisher:ZenodoFunded by:UKRI | REMS: Rigorous Engineerin..., EC | RustBelt, EC | ELVER

Authors: Rodolphe Lepigre; Michael Sammler; Kayvan Memarian; Robbert Krebbers; Derek Dreyer; Peter Sewell;

doi: 10.5281/zenodo.5662348 , 10.5281/zenodo.5662349

Artifact and Appendix of "VIP: Verifying Real-World C Idioms with Integer-Pointer Casts"

- Summary
- Subjects
- Metrics

Abstract

This is the artifact for the POPL'22 paper "VIP: Verifying Real-World C Idioms with Integer-Pointer Casts". It contains an extended version of the RefinedC and Cerberus tools with the presented VIP memory model, as well as examples, evaluation data, and the technical appendix for the paper.

Related Organizations

Max Planck Society
Germany
University of Cambridge
United Kingdom
THE CHANCELLOR, MASTERS AND SCHOLARS OF THE UNIVERSITY OF CAMBRIDGE
United Kingdom
Radboud University Nijmegen
Netherlands

Keywords

Separation logic, Proof automation, Pointer provenance, Memory model, Iris, Coq, C programming language

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	1
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average