Jacobs, Bart and Vogels, Frédéric and Piessens, Frank - Featherweight VeriFast

lmcs:1595 - Logical Methods in Computer Science, September 22, 2015, Volume 11, Issue 3
Featherweight VeriFast

Authors: Jacobs, Bart and Vogels, Frédéric and Piessens, Frank

VeriFast is a leading research prototype tool for the sound modular verification of safety and correctness properties of single-threaded and multithreaded C and Java programs. It has been used as a vehicle for exploration and validation of novel program verification techniques and for industrial case studies; it has served well at a number of program verification competitions; and it has been used for teaching by multiple teachers independent of the authors. However, until now, while VeriFast's operation has been described informally in a number of publications, and specific verification techniques have been formalized, a clear and precise exposition of how VeriFast works has not yet appeared. In this article we present for the first time a formal definition and soundness proof of a core subset of the VeriFast program verification approach. The exposition aims to be both accessible and rigorous: the text is based on lecture notes for a graduate course on program verification, and it is backed by an executable machine-readable definition and machine-checked soundness proof in Coq.


Source : oai:arXiv.org:1507.07697
DOI : 10.2168/LMCS-11(3:19)2015
Volume: Volume 11, Issue 3
Published on: September 22, 2015
Submitted on: August 18, 2014
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 83 times.
This article's PDF has been downloaded 32 times.