Sökning: "Interactive Theorem Prover"

Visar resultat 1 - 5 av 12 avhandlingar innehållade orden Interactive Theorem Prover.

  1. 1. A Verified Theorem Prover for Higher-Order Logic

    Författare :Oskar Abrahamsson; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; formal verification; higher-order logic; interactive theorem provers;

    Sammanfattning : This thesis is about mechanically establishing the correctness of computer programs. In particular, we are interested in establishing the correctness of tools used in computer-aided mathematics. We build on tools for proof-producing program synthesis, and verified compilation, and a verified theorem proving kernel. LÄS MER

  3. 2. Towards a Trustworthy Stack: Formal Verification of Low-Level Hardware and Software

    Författare :Ning Dong; Roberto Guanciale; Mads Dam; Magnus Myreen; KTH; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Formal Verification; Information Flow; Refinement; Interactive Theorem Prover; HOL4; Serial Interface; Pipelined Processor; Microarchitecture; Out-of-order Execution; Formell Verifiering; Informationsflöde; Förfining; Interaktiva Bevisprogrammet; HOL4; Seriellt Gränssnitt; Pipelined Processor; Mikroarkitektur; Omordnad Exekvering; Datalogi; Computer Science;

    Sammanfattning : Computer systems, consisting of hardware and software, have gained significant importance in the digitalised world. These computer systems rely on critical components to provide core functionalities and handle sensitive data. LÄS MER

  4. 3. Automated Theorem Proving in a First-Order Logic with First class Boolean Sort

    Författare :Evgenii Kotelnikov; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; first-order logic; program analysis; program verification; TPTP; automated theorem proving; Vampire;

    Sammanfattning : Automated theorem proving is one of the central areas of computer mathematics. It studies methods and techniques for establishing validity of mathematical problems using a computer. The problems are expressed in a variety of formal logics, including first-order logic. LÄS MER

  5. 4. Formalising process calculi

    Författare :Jesper Bengtson; Joachim Parrow; Daniel Hirschkoff; Uppsala universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; process calculi; interactive theorem proving; nominal logic; pi-calculus; CCS; psi-calculi; Computer science; Datalogi; Datavetenskap; Computer Science;

    Sammanfattning : As the complexity of programs increase, so does the complexity of the models required to reason about them. Process calculi were introduced in the early 1980s and have since then been used to model communication protocols of varying size and scope. LÄS MER

  7. 5. Induction Rules for Proving Correctness of Imperative Programs

    Författare :Angela Wallenburg; Göteborgs universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; program verification; software testing; interactive theorem proving; mathematical induction; customised induction rules;

    Sammanfattning : This thesis is aimed at simplifying the user-interaction in semi-interactive theorem proving for imperative programs. More specifically, we describe the creation of customised induction rules that are tailor-made for the specific program to verify and thus make the resulting proof simpler. LÄS MER