Formal verification of a C programme can be done (e.g.) by specifying the components of the programme in the ANSI/ISO C Specification Language (ACSL). To ease such work, formal verification tools can provide useful additional features. One potentially-useful feature that ACSL does not have is uninterpreted predicates. In this thesis, we looked at an existing implementation of ACSL based on constrained Horn clauses (CHCs), namely TriCera. We extended this implementation to support uninterpreted predicates based on existing support for the functionality in the underlying tool. The resulting implementation is able to solve for uninterpreted predicates in ACSL contracts.

Ett tillvägagångssätt för formell verifiering av ett C-program är att specificera program- komponenterna i ACSL (eng. ANSI/ISO C Specification Language). För att underlätta denna typ av arbete kan de verktyg som används i verifieringsprocessen erbjuda använd- bar funktionalitet utöver det som innefattas av ACSL. Ett exempel på sådan funktiona- litet är otolkade predikat (eng. uninterpreted predicates). I den här uppsatsen betraktade vi en existerande ACSL-implementation, TriCera, baserad på CHC:er (eng. constrained Horn clauses). Vi utökade implementationen med stöd för otolkade predikat genom att utnyttja existerande stöd för funktionaliteten i det underliggande verktyget. Detta resulterade i en implementation kapabel att lösa ut otolkade predikat i kontrakt.