Search for dissertations about: "Theorem Proving"

Showing result 6 - 10 of 43 swedish dissertations containing the words Theorem Proving.

2. 6. Proving and Disproving in Dynamic Logic for Java

   Author : Philipp Rümmer; Göteborgs universitet; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; theorem proving; disproving; dynamic logic; program verification; testing;

   Abstract : This thesis is about proving the functional correctness and incorrectness of imperative, object-oriented programs. One of the main approaches for the first item is deductive program verification, whereas the second item is traditionally handled by techniques like testing. READ MORE

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

   Author : Evgenii Kotelnikov; Chalmers tekniska högskola; []
   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

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

   Author : Angela Wallenburg; Göteborgs universitet; []
   Keywords : 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

6. 9. Deductive Program Analysis with First-Order Theorem Provers

   Author : Simon Robillard; Chalmers tekniska högskola; []
   Keywords : HUMANIORA; HUMANITIES; NATURVETENSKAP; NATURAL SCIENCES; TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; Automated theorem proving; Program semantics; Program Verification; Program analysis; Automated reasoning; First-order logic;

   Abstract : Software is ubiquitous in nearly all aspects of human life, including safety-critical activities. It is therefore crucial to analyze programs and provide strong guarantees that they perform as expected. READ MORE

7. 10. Analysis of Iterative or Recursive Programs Using a First-Order Theorem Prover

   Author : Simon Robillard; Chalmers tekniska högskola; []
   Keywords : NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; Term Algebras; Automated Theorem Proving; Invariant Generation; Program Verification;

   Abstract : Static analysis of program semantics can be used to provide strong guarantees about the correctness of software systems. In this thesis, we explore ways to perform automated program analysis and verification using a first-order theorem prover. READ MORE