Essays about: "Program verification"

Showing result 16 - 20 of 111 essays containing the words Program verification.

  1. 16. Parameterized Verification under The Total Store Order Memory Modelis EXPTIME-Complete

    University essay from Uppsala universitet/Institutionen för informationsteknologi

    Author : Yacoub Hendi; [2021]
    Keywords : ;

    Abstract : In this paper, we study the problem of parameterized verification of a concurrent program running under the Total Store Order (TSO) memory  model. A concurrent program is a finite set of processes that are instances of the same pushdown system and which communicate through a set of shared variables. READ MORE

  3. 17. Simple formally verified compiler in Lean

    University essay from Uppsala universitet/Institutionen för informationsteknologi

    Author : Leo Okawa Ericson; [2021]
    Keywords : ;

    Abstract : Computer checked proofs that a compiler is correct are important for increasing the confidence in programs. This report presents a simple compiler and a proof that the compiler is correct for terminating evaluations using the interactive theorem prover Lean, based on Concrete Semantics: with Isabelle/HOL. READ MORE

  4. 18. μSPL - Proprietary Graphics Language Transpiler : Asserting translation correctness using runtime verification

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

    Author : Henrik Andersson Glass; [2021]
    Keywords : Cockpit Display System; Compiler Correctness; Compiler; Transpiler; Computer Graphics; Cockpitpresentationssystem; Kompilatorkorrekthet; Kompilator; Transpilator; Datorgrafik;

    Abstract : The Swedish Armed Forces are currently considering extending the operational life of the Saab JAS 39 Gripen C/D multirole fighter aircraft by an additional 10 to 20 years. This has resulted in a need to upgrade many of the hardware components originally developed in the late 1980s and early 1990s. READ MORE

  5. 19. Plant Model Generator from Digital Twin for Purpose of Formal Verification

    University essay from Luleå tekniska universitet/Institutionen för system- och rymdteknik

    Author : Johannes Håkansson; [2021]
    Keywords : Digital twin; Plant verification; Model checking; Functional properties;

    Abstract : This master thesis will cover a way to automatically generate a formal model for plant verification from plant traces. The solution will be developed from trace data, stemming from a model of a digital twin of a physical plant. READ MORE

  6. 20. Proof-producing resolution of indirect jumps in the binary intermediate representation BIR

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

    Author : Adrian Westerberg; [2021]
    Keywords : Formal verification; Binary analysis; Interactive theorem proving; Indirect jump resolution; Formell verifiering; Binär analys; Interaktiv teorembevisning; Indirekt hopp bestämning;

    Abstract : HolBA is a binary analysis library that can be used to formally verify binary programs using contracts. It is developed in the interactive theorem prover HOL4 to achieve a high degree of trust in verification, the result of verification is a machine-checked proof demonstrating its correctness. This thesis presents two proof-producing procedures. READ MORE