Search for dissertations about: "theorem proving"

Showing result 1 - 5 of 43 swedish dissertations containing the words theorem proving.

2. 1. Verification of Distributed Erlang Programs using Testing, Model Checking and Theorem Proving

   Author : Hans Svensson; Chalmers tekniska högskola; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; distributed algorithms; fault-tolerance; theorem proving; verification; distributed programming; Erlang; model checking; testing;

   Abstract : Software infiltrates every aspect of modern society. Production, transportation, entertainment, and almost every other sphere that influences modern living are either directly or indirectly dependent on software systems. READ MORE

4. 2. Automated Theorem Proving with Extensions of First-Order Logic

   Author : Evgenii Kotelnikov; Chalmers tekniska högskola; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; clausal normal form; Program Verification; automated theorem proving; program analysis; TPTP; Vampire; first-order logic;

   Abstract : Automated theorem provers are computer programs that check whether a logical conjecture follows from a set of logical statements. The conjecture and the statements are expressed in the language of some formal logic, such as first-order logic. READ MORE

5. 3. Proving Safety and Security of Binary Programs

   Author : Andreas Lindner; Roberto Guanciale; Mads Dam; Tamara Rezk; KTH; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; Binary Code; Binary Analysis; Formal Verification; Model-Based Testing; Theorem Proving; HOL4; Intermediate Language; Instruction Set Architectures; ISA; Observational Models; Symbolic Execution; Weakest-Precondition; Execution Time Analysis; binärkod; binärkodsanalys; formell verifiering; modellbaserad testning; satsbevisning; HOL4; mellankod; instruktionsuppsättningar; ISA; observationsmodeller; symbolisk exekvering; minst restriktiva villkoret; analys av övre tidsgräns; Datalogi; Computer Science;

   Abstract : With the increasing ubiquity of computing devices, their correct and secure operation is of growing importance. In particular, critical components that provide core functionalities or process sensitive data have to operate as intended. READ MORE

6. 4. Theory Exploration and Inductive Theorem Proving

   Author : Dan Rosén; Chalmers tekniska högskola; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES;

   Abstract : We have built two state-of-the-art inductive theorem provers named HipSpec and Hipster. The main issue when automating proofs by induction is to discover essential helper lemmas. Our theorem provers use the technique theory exploration, which is a method to systematically discover interesting conclusions about a mathematical theory. READ MORE

7. 5. Stålmarck's Method for Automated Theorem Proving in First Order Logic

   Author : Magnus Björk; Chalmers tekniska högskola; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; automated theorem proving; Stålmarck s method; tableaux; first order logic;

   Abstract : We present an extension of Stålmarck's method to classical first order predicate logic. Stålmarck's method is a satisfiability checking method for propositional logic, and it resembles tableaux and KE. Its most distinctive feature is the dilemma rule, which is an extended branching rule, that allows branches to be recombined. READ MORE