Search for dissertations about: "interactive theorem proving"

Found 5 swedish dissertations containing the words interactive theorem proving.

  1. 1. Induction Rules for Proving Correctness of Imperative Programs

    University dissertation from Göteborg : Chalmers University of Technology

    Author : Angela Wallenburg; Göteborgs universitet.; Gothenburg University.; Göteborgs universitet.; Gothenburg University.; [2004]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; program verification; software testing; interactive theorem proving; mathematical induction; customised induction rules;

    Abstract : 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. READ MORE

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

    University dissertation from Göteborg : Chalmers University of Technology

    Author : Evgenii Kotelnikov; [2016]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES; first-order logic; program analysis; program verification; TPTP; automated theorem proving; Vampire;

    Abstract : 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. READ MORE

  3. 3. Formalising process calculi

    University dissertation from Uppsala : Acta Universitatis Upsaliensis

    Author : Jesper Bengtson; Uppsala universitet.; Uppsala universitet.; [2010]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES; process calculi; interactive theorem proving; nominal logic; pi-calculus; CCS; psi-calculi; TECHNOLOGY Information technology Computer science Computer science; TEKNIKVETENSKAP Informationsteknik Datavetenskap Datalogi; Computer Science; Datavetenskap;

    Abstract : 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. READ MORE

  4. 4. Static Analysis and Deductive Verification of Programs

    University dissertation from Uppsala : Acta Universitatis Upsaliensis

    Author : Tobias Gedell; [2006]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES;

    Abstract : This thesis is concerned with analysis of programs. Analysis of programs can be divided into two camps: static analysis and formal verification.Static program analyses compute a result and terminate for all programs. READ MORE

  5. 5. Formal Development of Safe and Secure Java Card Applets

    University dissertation from Uppsala : Acta Universitatis Upsaliensis

    Author : Wojciech Mostowski; [2005]
    Keywords : NATURVETENSKAP; NATURAL SCIENCES; object-oriented design; Java Card; formal verification; formal specification; dynamic logic;

    Abstract : This thesis is concerned with formal development of Java Card applets. Java Card is a technology that provides a means to program smart cards with (a subset of) the Java language. In recent years Java Card technology gained great interest in the formal verification community. There are two reasons for this. READ MORE