Provided by: AvocSoft
Date Added: Jan 2013
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.