Contract-Based Verification in TriCera

Abstract: Contracts are a powerful construct for programmers to communicate intent with functions, focusing on the what rather than the how. In this thesis, we move contracts from being just a form of communication to also have them define what it means for a software to be correct, and apply formal verification techniques to verify that contracts are never violated. We show how contract annotations written in the ANSI C Specification Language can be translated into suitable logical formulae, and show further how such formulae can be used when encoding a program into constrained Horn clauses. We provide an implementation following such steps by extending TriCera, a state-of-the-art verifier for C programs, to support contract annotations. Our additions pave the way for a contract-based, modular, verification process, and provide users of TriCera with a powerful tool for specifying correctness criteria.