Sökning: "program verification"

Visar resultat 1 - 5 av 150 uppsatser innehållade orden program verification.

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

   Kandidat-uppsats, Uppsala universitet/Institutionen för informationsteknologi

   Författare :Axel Bergström; [2023]
   Nyckelord :;

   Sammanfattning : 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. LÄS MER

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

4. 3. Verifiering av ny extraktionsmetod för analys på oljeindex

   Uppsats för yrkesexamina på grundnivå, KTH/Skolan för kemi, bioteknologi och hälsa (CBH)

   Författare :Theodor Hägglund; [2023]
   Nyckelord :metodverifiering; oljeindex; gaskromatografi; extraktion;

   Sammanfattning : Huvudsyftet med detta examensarbete var att verifiera en ny metod för extraktion av olja från jord-, slam-, och sedimentprover som ska ersätta företagets befintliga metod. Extraktionen sker på ett skakbord som förbehandling innan den extraherade oljan sätts på en GC-FID för att analysera dess oljeindex mellan C10-C40 samt dess olika specifika delfraktioner. LÄS MER

5. 4. Automated Inference of ACSL Contracts for Programs with Heaps

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

   Författare :Oskar Söderberg; [2023]
   Nyckelord :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;

   Sammanfattning : 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. LÄS MER

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

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

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

   Sammanfattning : 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. LÄS MER