Sökning: "Interactive theorem prover"

Visar resultat 6 - 7 av 7 uppsatser innehållade orden Interactive theorem prover.

  1. 6. Provably Sound and Secure Automatic Proving and Generation of Verification Conditions

    Master-uppsats, KTH/Teoretisk datalogi, TCS

    Författare :Didrik Lundberg; [2018]
    Nyckelord :HOL4; HOL; Higher-order logic; SML; Poly ML; Formal methods; Axiomatic semantics; Formal verification; Static verification; Program verification; Hoare logic; Floyd-Hoare logic; ITP; Interactive theorem prover; Theorem prover; Proof assistant; BIR; Automated theorem proving; ATP; Automated deduction; Computer-assisted proof; Automated reasoning;

    Sammanfattning : Formal verification of programs can be done with the aid of an interactive theorem prover. The program to be verified is represented in an intermediate language representation inside the interactive theorem prover, after which statements and their proofs can be constructed. This is a process that can be automated to a high degree. LÄS MER

  3. 7. Verifying Psi-calculi

    Magister-uppsats, Institutionen för informationsteknologi

    Författare :Johannes Åman Pohjola; [2010]
    Nyckelord :;

    Sammanfattning : Psi-calculi are mobile process calculi, parametrised with arbitrary nominal datatypes representing data, communication channels, assertions and conditions, as well as morphisms over those datatypes. The framework for psi-calculi has been formalised in the interactive theorem prover Isabelle, along with both strong and weak bisimulation. LÄS MER