Sökning: "verification theorem"

Visar resultat 1 - 5 av 37 avhandlingar innehållade orden verification theorem.

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

   Författare :Hans Svensson; Chalmers University of Technology; []
   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. 2. Secure System Virtualization : End-to-End Verification of Memory Isolation

   Författare :Hamed Nemati; Mads Dam; Gustavo Betarte; KTH; []
   Nyckelord :NATURAL SCIENCES; NATURVETENSKAP; NATURVETENSKAP; NATURAL SCIENCES; Platform Security; Hypervisor; Formal Verification; Theorem Proving; HOL4; Cache attack; Security Monitor; Information Flow; Computer Science; Datalogi;

   Sammanfattning : Over the last years, security-kernels have played a promising role in reshaping the landscape of platform security on embedded devices. Security-kernels, such as separation kernels, enable constructing high-assurance mixed-criticality execution platforms on a small TCB, which enforces isolation between components. LÄS MER

4. 3. Formal Verification of Peripheral Memory Isolation

   Författare :Jonas Haglund; Roberto Guanciale; Mads Dam; Gligor Virgil; KTH; []
   Nyckelord :ENGINEERING AND TECHNOLOGY; TEKNIK OCH TEKNOLOGIER; TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; formal verification; interactive theorem proving; direct memory access; memory isolation; input output; formell verifiering; interaktiv datorassisterad beviskonstruktion; direkt minnesåtkomst; minnesisolering; indata utdata; Datalogi; Computer Science;

   Sammanfattning : In many contexts, computers run both critical and untrusted software,necessitating the need for isolating critical software from untrusted software.These computers contain CPUs, memory and peripherals. LÄS MER

5. 4. Few is Just Enough! : Small Model Theorem for Parameterized Verification and Shape Analysis

   Författare :Frédéric Haziza; Parosh Aziz Abdulla; Tomáš Vojnar; Uppsala universitet; []
   Nyckelord :ENGINEERING AND TECHNOLOGY; TEKNIK OCH TEKNOLOGIER; TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; program verification; model checking; parameterized systems; infinite-state systems; reachability; approximation; safety; tree systems; shape analysis; small model properties; view abstraction; monotonic abstraction; Computer Science; Datavetenskap;

   Sammanfattning : This doctoral thesis considers the automatic verification of parameterized systems, i.e. systems with an arbitrary number of communicating components, such as mutual exclusion protocols, cache coherence protocols or heap manipulating programs. The components may be organized in various topologies such as words, multisets, rings, or trees. LÄS MER

7. 5. A Verified Theorem Prover for Higher-Order Logic

   Författare :Oskar Abrahamsson; Chalmers University of Technology; []
   Nyckelord :formal verification; higher-order logic; interactive theorem provers;

   Sammanfattning : This thesis is about mechanically establishing the correctness of computer programs. In particular, we are interested in establishing the correctness of tools used in computer-aided mathematics. We build on tools for proof-producing program synthesis, and verified compilation, and a verified theorem proving kernel. LÄS MER