CW 638
Gijs Vanspauwen and Bart JacobsVeriFast: Sound symbolic linking in the presence of preprocessing
Abstract
Formal verification enables developers to provide safety and security guarantees about their code. A modular verification approach supports the verification of different pieces of an application in separation. VeriFast is an annotation-based verifier for C source code that implements symbolic linking to support modular verification. This report describes the process of symbolic linking and the unsoundness introduced by the C preprocessor. Moreover it contains a detailed formalization of our solution and a proof of its correctness.
report.pdf (445K) / mailto: G. Vanspauwen