Sökning: "Interaktiv teorembevisning"

Hittade 1 uppsats innehållade orden Interaktiv teorembevisning.

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