Software Verification with VeriFast: Industrial Case Studies

In this paper, the authors present a series of four industrial case studies in software verification. They applied VeriFast, a sound and modular software verifier 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. Their case studies have been carefully selected so as to evaluate the industrial applicability of VeriFast. They 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.

Provided by: AvocSoft Topic: Security Date Added: Jan 2013 Format: PDF

Find By Topic