Essays about: "program verification"

Showing result 1 - 5 of 111 essays containing the words program verification.

  1. 1. Adding Basic Support for Function Pointers in TriCera

    University essay from Uppsala universitet/Institutionen för informationsteknologi

    Author : Axel Bergström; [2023]
    Keywords : ;

    Abstract : TriCera is a verification tool that encodes programs in a C-like language to a set of Constrained Horn Clauses.  These clauses describe the program states that can be reached when the program is executed.  A solver can then be used to check if the program is safe. READ MORE

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

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

  5. 4. An Empirical Study on Using Codex for Automated Program Repair

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

    Author : Pengyu Zhao; [2023]
    Keywords : Automated Program Repair; Codex; Large Language Models; Defects4J; Patch Generation; Prompt Engineering; Automatiserad Programreparation; Codex; Storskaliga Språkmodeller; Defects4J; Patchgenerering; Promptteknik;

    Abstract : This thesis explores the potential of Codex, a pre-trained Large Language Model (LLM), for Automated Program Repair (APR) by assessing its performance on the Defects4J benchmark that includes real-world Java bugs. The study aims to provide a comprehensive understanding of Codex’s capabilities and limitations in generating syntactically and semantically equivalent patches for defects, as well as evaluating its ability to handle defects with different levels of importance and complexity. READ MORE

  6. 5. The Global Interconnection Scheme of Silago : RTL Design and Verification

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

    Author : Tong Lou; [2023]
    Keywords : Silago; global interconnection; synchronous dataflow; network on chip; Silago; global sammankoppling; synkront dataflöde; nätverk på chip;

    Abstract : The Silago concept introduces a hardware-centric platform that is based on coarse-grained reconfigurable fabrics and networks on chips(NoCs). With the intra-region and inter-region NoC, the Silago platform can form resource clusters to host various applications. READ MORE