Sökning: "proving"

Visar resultat 1 - 5 av 215 avhandlingar innehållade ordet proving.

1. 1. Proving Safety and Security of Binary Programs

   Författare :Andreas Lindner; Roberto Guanciale; Mads Dam; Tamara Rezk; KTH; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Binary Code; Binary Analysis; Formal Verification; Model-Based Testing; Theorem Proving; HOL4; Intermediate Language; Instruction Set Architectures; ISA; Observational Models; Symbolic Execution; Weakest-Precondition; Execution Time Analysis; binärkod; binärkodsanalys; formell verifiering; modellbaserad testning; satsbevisning; HOL4; mellankod; instruktionsuppsättningar; ISA; observationsmodeller; symbolisk exekvering; minst restriktiva villkoret; analys av övre tidsgräns; Datalogi; Computer Science;

   Sammanfattning : With the increasing ubiquity of computing devices, their correct and secure operation is of growing importance. In particular, critical components that provide core functionalities or process sensitive data have to operate as intended. LÄS MER

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

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

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

4. 3. Testing and Proving using Narrowing

   Författare :Fredrik Lindblad; Göteborgs universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; program correctness; software testing; formal verification; proof construction; dependent types; type theory; narrowing; dependent types;

   Sammanfattning : In order to know if a program is correct a specification of its intended behaviour must be stated. The two main activities concerning program correctness are testing and verification. LÄS MER

5. 4. Exercising Mathematical Competence: Practising Representation Theory and Representing Mathematical Practice

   Författare :Anna Ida Säfström; Göteborgs universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; NATURVETENSKAP; NATURAL SCIENCES; SAMHÄLLSVETENSKAP; SOCIAL SCIENCES; Mathematical competence; exercising competencies; young children; whole number arithmetic; tertiary level; proving; highest weight representation; tensor product decomposition; skew-symmetric matrix; moment map; infinite dimensional unitary representation; highest weight representation;

   Sammanfattning : This thesis assembles two papers in mathematics and two papers in mathematics education. In the mathematics part, representation theory is practised. Two Clebsch-Gordan type problems are addressed. LÄS MER

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

   Författare :Angela Wallenburg; Göteborgs universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; program verification; software testing; interactive theorem proving; mathematical induction; customised induction rules;

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