Search for dissertations about: "proving"

Showing result 21 - 25 of 208 swedish dissertations containing the word proving.

2. 21. Formal Verification of Peripheral Memory Isolation

   Author : Jonas Haglund; Roberto Guanciale; Mads Dam; Gligor Virgil; KTH; []
   Keywords : TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; formal verification; interactive theorem proving; direct memory access; memory isolation; input output; formell verifiering; interaktiv datorassisterad beviskonstruktion; direkt minnesåtkomst; minnesisolering; indata utdata; Datalogi; Computer Science;

   Abstract : In many contexts, computers run both critical and untrusted software,necessitating the need for isolating critical software from untrusted software.These computers contain CPUs, memory and peripherals. READ MORE

4. 22. Quantifiers and Theories : A Lazy Approach

   Author : Peter Backeman; Philipp Rümmer; Jie-Hong Roland Jiang; Uppsala universitet; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; Automated Reasoning; Automated Theorem Proving; SMT; Unification; Datavetenskap med inriktning mot inbyggda system; Computer Science with specialization in Embedded Systems;

   Abstract : In this thesis we study Automated Theorem Proving (ATP) as well as Satisfiability Modulo Theories (SMT) and present lazy strategies for improving reasoning within these areas. A lazy strategy works by simplifying a problem, and gradually refines the abstraction only when necessary. READ MORE

5. 23. Formalising process calculi

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

   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

6. 24. A First Order Extension of Stålmarck's Method

   Author : Magnus Björk; Chalmers tekniska högskola; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; Tableaux; Automated Theorem Proving; Stålmarck s Method;

   Abstract : Stålmarck's method is an algorithm that decides validity of formulae in propositional logic. It resembles many tableaux method, but uses a special branch-and-merge-rule, called the dilemma rule. The dilemma rule creates two branches, where a formula (called the dilemma formula) is assumed to be false in one branch and true in the other one. READ MORE

7. 25. Building Verified Hardware and Verified Stacks in HOL

   Author : Andreas Lööw; Chalmers tekniska högskola; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; hardware synthesis; compilers; formal verification; interactive theorem proving;

   Abstract : This thesis explores building provably correct software and hardware inside the HOL4 interactive theorem prover. Interactive theorem provers such as HOL4 are proof environments where manual (human) and automated (machine) proofs can be composed in logically safe ways and all proof steps (be it manual or automated) are mechanically checked. READ MORE