Sökning: "model-checker"

Visar resultat 1 - 5 av 38 uppsatser innehållade ordet model-checker.

  1. 1. Automated Inference of ACSL Contracts for Programs with Heaps

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

    Författare :Oskar Söderberg; [2023]
    Nyckelord :Formal Verification; Contract Inference; Model Checking; Deductive Verification; Theory of Heaps; ACSL; Translation; Formell Verifiering; Kontrakth¨arledning; Modellprovning; Deduktiv Verifiering; Theory of Heaps; ACSL; Overs¨attning;

    Sammanfattning : Contract inference consists in automatically computing contracts that formally describe the behaviour of program functions. Contracts are used in deductive verification, which is a method for verifying whether a system behaves according to a provided specification. The Saida plugin in Frama-C is a contract inference tool for C code. LÄS MER

  3. 2. Application of formal verification and validation on modern multi-functional signalling system

    Master-uppsats, KTH/Transportplanering

    Författare :Shamsul Arefin; [2022]
    Nyckelord :;

    Sammanfattning : Demand for rail transport is increasing day by day. Rail is popular in public transport due to punctuality, regularity, and safety. However, we hear daily that rail traffic still has many problems to solve about incidents, near misses, and signal errors. LÄS MER

  4. 3. Standardiserad kvalitetssäkring av brandskydd i BIM

    Kandidat-uppsats, Lunds universitet/Avdelningen för Brandteknik

    Författare :Mathias Undeland; Oliwer Warnerfelt; [2022]
    Nyckelord :BIM; Byggnadsinformationsmodellering; Solibri Office; Solibri Model Checker; SMC; brandprojektering; digital projektering; kvalitetskontroll; kvalitetssäkring; BIMfire Tools.; Technology and Engineering;

    Sammanfattning : Digitized workflows are becoming more common in the construction industry where building information modeling, also called BIM, is a common example of this development. The BIM environment enables an unbroken chain of information on a corporate platform. LÄS MER

  5. 4. Filtering equivalent changes from dependency updates with CBMC

    Uppsats för yrkesexamina på avancerad nivå, Blekinge Tekniska Högskola/Institutionen för datavetenskap

    Författare :Jonas Mårtensson; [2022]
    Nyckelord :CBMC; change impact analysis; equivalence analysis; auto-generation; CBMC; konsekvensanalys; ekvivalensanalys; autogenerering;

    Sammanfattning : Background. Open source dependencies have become ubiquitous in software development and the risk of regressions during an update are a key concern facing developers. Change impact analysis (CIA) can be used to assess the effects of a dependency update and aid in addressing this challenge. LÄS MER

  7. 5. Compiler Testing of C11 Atomics for Arm and RISC-V

    Uppsats för yrkesexamina på avancerad nivå, Uppsala universitet/Datorteknik

    Författare :Hampus Adolfsson; [2022]
    Nyckelord :compiler; compiler testing; atomics; c11 atomics; arm; risc-v;

    Sammanfattning : The C11 standard introduced atomic types and operations, with an accompanying memory model, to enable the use of shared variables in concurrent programs. In this thesis, I demonstrate how compilers can be tested, in a way that is deterministic and covers the entire set of atomic operations, to ensure they correctly implement C11 atomics and the C11 memory model. LÄS MER