Sökning: "Kontraktgenerering"

Hittade 2 uppsatser innehållade ordet Kontraktgenerering.

  1. 1. Improving the Synthesis of Annotations for Partially Automated Deductive Verification

    Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Författare :Hovig Manjikian; [2023]
    Nyckelord :Formal verification; Automated verification; Contract inference.; Formell verifiering; Automatiserad verifiering; Kontraktgenerering.;

    Sammanfattning : This work investigates possible improvements to an existing annotation inference tool. The tool is part of a toolchain that aims to automate the process of software verification using formal methods. LÄS MER

  3. 2. Automated inference of ACSL function contracts using TriCera

    Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Författare :Jesper Amilon; [2021]
    Nyckelord :Formal Verification; Contract inference; Hoare Logic; Model Checking; Horn clauses; Formell verifikation; Kontraktgenerering; Formell semantik; Hoare logik; Modellprovning; Horn clauses;

    Sammanfattning : This thesis explores synergies between deductive verification and model checking, by using the existing model checker TriCera to automatically infer specifications for the deductive verifier Frama-C. To accomplish this, a formal semantics is defined for a subset of ANSI C, extended with assume statements, called Csmall. LÄS MER