Essays about: "Modellprovning"

Found 3 essays containing the word Modellprovning.

  1. 1. 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

  3. 2. 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

  4. 3. Implementation and evaluation of bounded invariant model checking for a subset of Stateflow

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

    Author : Gustav Ung; [2021]
    Keywords : Formal methods; Bounded Model Checking; Stateflow; SLDV; Formella metoder; Begränsad modellprovning; Stateflow; SLDV;

    Abstract : Stateflowmodels are used for describing logic and implementing state machines in modern safety-critical software. However, the complete Stateflowmodelling language is hard to formally define, therefore a subset relevant for industrial models has been developed in previous works. READ MORE