Essays about: "Deductive Verification"

Showing result 1 - 5 of 14 essays containing the words Deductive Verification.

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

    University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Author : Hovig Manjikian; [2023]
    Keywords : Formal verification; Automated verification; Contract inference.; Formell verifiering; Automatiserad verifiering; Kontraktgenerering.;

    Abstract : 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. READ MORE

  3. 2. Automated Inference of ACSL Contracts for Programs with Heaps

    University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Author : Oskar Söderberg; [2023]
    Keywords : Formal Verification; Contract Inference; Model Checking; Deductive Verification; Theory of Heaps; ACSL; Translation; Formell Verifiering; Kontrakth¨arledning; Modellprovning; Deduktiv Verifiering; Theory of Heaps; ACSL; Overs¨attning;

    Abstract : Contract inference consists in automatically computing contracts that formally describe the behaviour of program functions. Contracts are used in deductive verification, which is a method for verifying whether a system behaves according to a provided specification. The Saida plugin in Frama-C is a contract inference tool for C code. READ MORE

  4. 3. A Comparative Study on Deductive Verification for Rust and C

    University essay from KTH/Datavetenskap

    Author : Nils Löfberg; Aron Bergman; [2022]
    Keywords : ;

    Abstract : In programming, deductive verification is a technique to generate proof that a function obeys a set of manually specified regulations in the form of annotations. In addition to these annotations, the verifier also utilizes the constraints of the underlying programming language to prove that the function cannot cause the program to crash unexpectedly. READ MORE

  5. 4. Synthesis of Annotations for Partially Automated Deductive Verification

    University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Author : Daniel Skantz; [2021]
    Keywords : ;

    Abstract : We investigate the possibility of inferring annotations from source code to enable a partially automated process of deductive verification within the scope of embedded systems code. Specifically, we design a plugin for the verification framework Frama-C, that synthesizes function contracts including every precondition necessary to later prove functional software specifications. READ MORE

  6. 5. Automated inference of ACSL function contracts using TriCera

    University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Author : Jesper Amilon; [2021]
    Keywords : Formal Verification; Contract inference; Hoare Logic; Model Checking; Horn clauses; Formell verifikation; Kontraktgenerering; Formell semantik; Hoare logik; Modellprovning; Horn clauses;

    Abstract : 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. READ MORE