Sökning: "automated theorem proving"

Visar resultat 6 - 10 av 16 avhandlingar innehållade orden automated theorem proving.

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

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

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

  3. 7. 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

  4. 8. Theory Exploration for Programs and Proofs

    Författare :Sólrún Einarsdóttir; Chalmers tekniska högskola; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Theorem Proving; Automated Reasoning; Theory Exploration; Property-Based Testing; Functional Programming; Conjecture Generation; Artificial Intelligence; Coinduction;

    Sammanfattning : We have built two theory exploration systems, Cohipster and RoughSpec . Theory exploration is a method of automatically conjecturing properties about the functions and structures that appear in a computer program or a formalization of a mathematical theory. LÄS MER

  5. 9. Analysis of Iterative or Recursive Programs Using a First-Order Theorem Prover

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

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

  7. 10. No Hypervisor Is an Island : System-wide Isolation Guarantees for Low Level Code

    Författare :Oliver Schwarz; Mads Dam; Christian Gehrmann; Gerwin Klein; KTH; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Platform Security; Hypervisor; Formal Verification; Theorem Proving; HOL4; DMA; Peripheral Devices; Instruction Set Architectures; ISA; Information Flow; Boot; Computer Science; Datalogi;

    Sammanfattning : The times when malware was mostly written by curious teenagers are long gone. Nowadays, threats come from criminals, competitors, and government agencies. Some of them are very skilled and very targeted in their attacks. LÄS MER