Sökning: "satisfiability modulo theories"

Visar resultat 1 - 5 av 6 avhandlingar innehållade orden satisfiability modulo theories.

  1. 1. Quantifiers and Theories : A Lazy Approach

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

    Sammanfattning : 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. LÄS MER

  3. 2. Verification Based Failure Detection for Real-Time Java and Floating-Point Computations

    Författare :Gabriele Paganelli; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; Debugging; Floating-Point; Formal Methods; Testing; Real-Time Java; Coverage; Satisfiability Modulo Theories; Certification; Formal Specification;

    Sammanfattning : To err is human, and machines help us avoiding errors. This thesis presents two ways, based on verification technology, to prevent failures.Safety critical Real-Time Java applications usually need a certification. Tests fulfilling specific coverage criteria can be part of such certification, like in the DO-178 standard. LÄS MER

  4. 3. On Solving String Constraints

    Författare :Phi Diep Bui; Mohamed Faouzi Atig; Parosh Abdulla; Matthew Hague; Uppsala universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; String constraint solving; SMT; Verification;

    Sammanfattning : Software systems are deeply involved in diverse human activities as everyone uses a variety of software systems on a daily basis. It is essential to guarantee that software systems all work correctly. Two popular methods for finding failures of software systems are testing and model checking. LÄS MER

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

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

    Sammanfattning : 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. LÄS MER

  7. 5. Pattern-based Specification and Formal Analysis of Embedded Systems Requirements and Behavioral Models

    Författare :Predrag Filipovikj; Cristina Seceleanu; Guillermo Rodriguez-Navas; Stefania Gnesi; Mälardalens högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; pattern-based formal requirements specification; formal requirements consistency analysis; formal analysis of Simulink models; Computer Science; datavetenskap;

    Sammanfattning : Since the first lines of code were introduced in the automotive domain, vehicles have transitioned from being predominantly mechanical systems to software intensive systems. With the ever-increasing computational power and memory of vehicular embedded systems, a set of new, more powerful and more complex software functions are installed into vehicles to realize core functionalities. LÄS MER