VeriFast: Sound symbolic linking in the presence of preprocessing

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.nrpages: 32status: publishe