Title: Software verification with VeriFast: Industrial case studies
Authors: Philippaerts, Pieter ×
Mühlberg, Jan Tobias
Penninckx, Willem
Smans, Jan
Jacobs, Bart
Piessens, Frank #
Issue Date: 1-Mar-2014
Publisher: North-Holland Pub. Co.
Series Title: Science of Computer Programming vol:82 issue:1 pages:77-97
Article number: 6
Abstract: In this article we present a series of four industrial case studies in software verification. We applied VeriFast, a sound and modular software verier based on separation logic, to two Java Card smart card applets, a Linux device driver, and an embedded Linux network management component, the latter two written in C. Our case studies have been carefully selected so as to evaluate the industrial applicability of VeriFast. We focus on proving the absence of safety violations, e.g., that the programs do not perform illegal operations such as dividing by zero or illegal memory accesses. Yet, given the sensitive application environment of our case studies, these safety properties typically have security implications. In this article we give a detailed description of the VeriFast approach to software verification based on two of the above case studies, one in Java and one in C. Finally, we draw conclusions on the overall feasibility of using VeriFast to verify software components in industrial domains that have stringent requirements on reliability and security.
ISSN: 0167-6423
Publication status: published
KU Leuven publication type: IT
Appears in Collections:Informatics Section
Department of Health and Technology - UC Leuven
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
paper.pdf Published 368KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science