Search for dissertations about: "Philipp Rümmer"

Showing result 1 - 5 of 6 swedish dissertations containing the words Philipp Rümmer.

  2. 1. Calculi for Program Incorrectness and Arithmetic

    Author : Philipp Rümmer; Göteborgs universitet; []
    Keywords : NATURVETENSKAP; NATURAL SCIENCES;

    Abstract : This thesis is about the development and usage of deductive methods in two main areas: (i) the deductive dis-verification of programs, i.e., how techniques for deductive verification of programs can be used to detect program defects, and (ii) reasoning modulo integer arithmetic, i.e. READ MORE

  4. 2. 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

  5. 3. New techniques for handling quantifiers in Boolean and first-order logic

    Author : Peter Backeman; Philipp Rümmer; Uppsala universitet; []
    Keywords : NATURVETENSKAP; NATURAL SCIENCES; Datavetenskap med inriktning mot inbyggda system; Computer Science with specialization in Embedded Systems;

    Abstract : The automation of reasoning has been an aim of research for a long time. Already in 17th century, the famous mathematician Leibniz invented a mechanical calculator capable of performing all four basic arithmetic operators. READ MORE

  6. 4. 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

  7. 5. Model Checking of Software Systems under Weak Memory Models

    Author : Tuan-Phong Ngo; Mohamed Faouzi Atig; Parosh Aziz Abdulla; Philipp Rümmer; Viktor Vafeiadis; Uppsala universitet; []
    Keywords : TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; Model checking; Concurrent program; Weak memory model; Computer Science; Datavetenskap;

    Abstract : When a program is compiled and run on a modern architecture, different optimizations may be applied to gain in efficiency. In particular, the access operations (e.g., read and write) to the shared memory may be performed in an out-of-order manner, i. READ MORE