VeriFast: Sound Symbolic Linking in the Presence of Preprocessing

Download Now
Provided by: Katholieke Universiteit Leuven
Topic: Security
Format: PDF
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 the authors' solution and a proof of its correctness.
Download Now

Find By Topic