Sökning: "Horn clauses"

Hittade 5 uppsatser innehållade orden Horn clauses.

  1. 1. Contract-Based Verification in TriCera

    Master-uppsats, Uppsala universitet/Institutionen för informationsteknologi

    Författare :Pontus Ernstedt; [2022]
    Nyckelord :;

    Sammanfattning : Contracts are a powerful construct for programmers to communicate intent with functions, focusing on the what rather than the how. In this thesis, we move contracts from being just a form of communication to also have them define what it means for a software to be correct, and apply formal verification techniques to verify that contracts are never violated. LÄS MER

  3. 2. Exploring properties and limitations of Graph Neural Networks (GNNs) in Software Verification

    Kandidat-uppsats, Uppsala universitet/Institutionen för informationsteknologi

    Författare :Kexin Xu; [2021]
    Nyckelord :;

    Sammanfattning : This study analyzes how applicable Graph Neural Networks (GNNs) can be used for learning the labels of Horn graphs that are generated from Constrained Horn Clauses (CHCs) using Eldarica. To answer this question, 121 mono-direction edge layer graphs and hyper-edge graphs are prepared to be trained and validated and tested, weights per 10 epochs and losses are collected and visualized in 6 scenarios. LÄS MER

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

  5. 4. Elusive Depictions of Time : An analysis of Japanese temporal connectors expressing 'before'

    Kandidat-uppsats, Stockholms universitet/Institutionen för lingvistik

    Författare :Oscar Aspholm; [2019]
    Nyckelord :temporal connectors; temporal clauses; lexical aspect; semantics; Japanese; temporala konnektorer; temporala satser; lexikal aspekt; semantik; japanska;

    Sammanfattning : This study explores the two Japanese temporal connectors mae ni and nai uchi ni that express the notion of ‘before.’ These have been claimed to differ in factuality and certainty (Kuno, 1973) and on pragmatic grounds in the form of speaker attitude (Hasegawa, 2015). LÄS MER

  7. 5. At the Threat of Piracy - Hire Issues in Time Charterparties

    Uppsats för yrkesexamina på avancerad nivå, Lunds universitet/Juridiska institutionen

    Författare :Peter Hallin; [2010]
    Nyckelord :Standardavtal; Standard form; Deviation; Off-hire; Certeparti; Charter party; Sjörätt; Transporträtt; Law and Political Science;

    Sammanfattning : Allteftersom hotet från sjöröveri har växt under 2000-talet har rederinäringen tvingats hitta sätt att hantera och fördela riskerna. Denna uppsats behandlar branschens kanske främsta riskfördelningsinstrument (i förhållande till sjöröveri) – standardavtal och försäkringar. LÄS MER