Essays about: "model-checker"

Showing result 1 - 5 of 23 essays containing the word model-checker.

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

    University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Author : Oskar Söderberg; [2023]
    Keywords : 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;

    Abstract : 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. READ MORE

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

    University essay from KTH/Transportplanering

    Author : Shamsul Arefin; [2022]
    Keywords : ;

    Abstract : 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. READ MORE

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

    University essay from Blekinge Tekniska Högskola/Institutionen för datavetenskap

    Author : Jonas Mårtensson; [2022]
    Keywords : CBMC; change impact analysis; equivalence analysis; auto-generation; CBMC; konsekvensanalys; ekvivalensanalys; autogenerering;

    Abstract : 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. READ MORE

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

    University essay from Uppsala universitet/Datorteknik

    Author : Hampus Adolfsson; [2022]
    Keywords : compiler; compiler testing; atomics; c11 atomics; arm; risc-v;

    Abstract : 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. READ MORE

  6. 5. Multi-Agent Games of Imperfect Information: Algorithms for Strategy Synthesis

    University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Author : Viktor Åkerblom Jonsson; David Berisha; [2021]
    Keywords : Strategy Synthesis; Multi-Agent Knowledge- Based Subset Construction; Strategic Model Checker; Multi- Agent Games; Imperfect Information;

    Abstract : The aim of this project was to improve upon a toolfor strategy synthesis for multi-agent games of imperfect informationagainst nature. Another objective was to compare the toolwith the original tool we improved upon and the Strategic ModelChecker (SMC). READ MORE