Avancerad sökning

Visar resultat 1 - 5 av 7 uppsatser som matchar ovanstående sökkriterier.

  1. 1. A Verified QBF Solver

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

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

    Sammanfattning : Quantified Boolean Formulas (QBFs) extend propositional logic with universal and existential quantification over Boolean variables.  A QBF is satisfiable if and only if there is an assignment of Boolean values to the free variables that makes the formula true, and a QBF solver is a software tool determining if a given QBF is satisfiable. LÄS MER

  3. 2. Simple formally verified compiler in Lean

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

    Författare :Leo Okawa Ericson; [2021]
    Nyckelord :;

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

  4. 3. Proof-producing resolution of indirect jumps in the binary intermediate representation BIR

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

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

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

  5. 4. Verifying Correctness of Contract Decompositions

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

    Författare :Gustav Hedengran; [2020]
    Nyckelord :;

    Sammanfattning : The importance of verification in safety critical systems is well known. However, due to the complexity of verification, the task of formally verifying large safety-critical systems might prove computationally infeasible in many cases. Compositional verification is a technique aimed at enabling verification of large safety-critical systems. LÄS MER

  7. 5. Implementation and Verification of Sorting Algorithms with the Interactive Theorem Prover HOL

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

    Författare :Sara Quarfot Orrevall; [2020]
    Nyckelord :;

    Sammanfattning : As the world becomes increasingly reliant on technology and the technology becomes increasingly complex, ensuring software correctness is becoming both increasingly important and difficult. Methods like software testing are rarely enough to guarantee that a program will always work as intended. Formal methods offer attractive alternatives. LÄS MER