Sökning: "Formell semantik"

Hittade 4 uppsatser innehållade orden Formell semantik.

  1. 1. Reliable Web Applications Through Contracts and Generative Testing

    Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Författare :Fredrik Hallsmar; [2022]
    Nyckelord :Web applications; Design by contract; Generative testing; Reliability; Clojure; Webbapplikationer; Kontrakt; Automatisk testning; Pålitlighet; Clojure;

    Sammanfattning : Client-side web applications have recently gone from progressive enhancements to powering large scale Single-page Applications (SPAs). Testing such applications is a tedious effort, often requiring manually constructing tests and emulating the browser, which leads to high programming effort and low performance. LÄS MER

  3. 2. Automated inference of ACSL function contracts using TriCera

    Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Författare :Jesper Amilon; [2021]
    Nyckelord :Formal Verification; Contract inference; Hoare Logic; Model Checking; Horn clauses; Formell verifikation; Kontraktgenerering; Formell semantik; Hoare logik; Modellprovning; Horn clauses;

    Sammanfattning : This thesis explores synergies between deductive verification and model checking, by using the existing model checker TriCera to automatically infer specifications for the deductive verifier Frama-C. To accomplish this, a formal semantics is defined for a subset of ANSI C, extended with assume statements, called Csmall. LÄS MER

  4. 3. Relational Symbolic Execution in WebAssembly

    Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Författare :Johan Sjölén; [2020]
    Nyckelord :;

    Sammanfattning : WebAssembly is a new low-level language used as a compilation target which runs in web browsers. As more code is run on the client side of a web application the issue of security of that code become more important. LÄS MER

  5. 4. Deterministic Concurrency Using Lattices and the Object Capability Model

    Master-uppsats, KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Författare :Ellen Arvidsson; [2018]
    Nyckelord :type systems; concurrency; determinism; object capability model; lattices; small-step operational semantics;

    Sammanfattning : Parallelization is an important part of modern data systems. However, the non-determinism of thread scheduling introduces the difficult problem of considering all different execution orders when constructing an algorithm. Therefore deterministic-by-design concurrent systems are attractive. LÄS MER