Sökning: "infinite-state systems"

Visar resultat 1 - 5 av 16 avhandlingar innehållade orden infinite-state systems.

  1. 1. Infinite-state Stochastic and Parameterized Systems

    Detta är en avhandling från Uppsala : Acta Universitatis Upsaliensis

    Författare :Noomene Ben Henda; Uppsala universitet.; Uppsala universitet.; [2008]
    Nyckelord :program verification; model checking; stochastic games; infinite-state systems; Markov chains; reachability; repeated reachability; parameterized systems; approximation; safety; tree systems;

    Sammanfattning : A major current challenge consists in extending formal methods in order to handle infinite-state systems. Infiniteness stems from the fact that the system operates on unbounded data structure such as stacks, queues, clocks, integers; as well as parameterization. LÄS MER

  2. 2. Games and Probabilistic Infinite-State Systems

    Detta är en avhandling från Uppsala : Universitetsbiblioteket

    Författare :Sven Sandberg; Uppsala universitet.; Uppsala universitet.; [2007]
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; program verification; model checking; determinacy; strategy improvement; infinite games; parity games; mean payoff games; stochastic games; Büchi games; reachability games; limiting average; limiting behavior; Markov chains; infinite-state systems; lossy channel systems; vector addition systems; noisy Turing machines; TECHNOLOGY Information technology Computer science; TEKNIKVETENSKAP Informationsteknik Datavetenskap;

    Sammanfattning : Computer programs keep finding their ways into new safety-critical applications, while at the same time growing more complex. This calls for new and better methods to verify the correctness of software. We focus on one approach to verifying systems, namely that of model checking. LÄS MER

  3. 3. Verification of Infinite-State Systems : Decision Problems and Efficient Algorithms

    Detta är en avhandling från Department of Computer Systems, Uppsala University

    Författare :Mats Kindahl; Uppsala universitet.; [1999]
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Computer Systems; Datorteknik;

    Sammanfattning : This thesis presents methods for the verification of distributed systems with infinite state spaces. We consider several verification problems for lossy channel systems, a class of infinite-state systems consisting of finite-state machines that communicate over unbounded, but lossy, FIFO channels. LÄS MER

  4. 4. Few is Just Enough! Small Model Theorem for Parameterized Verification and Shape Analysis

    Detta är en avhandling från Uppsala : Acta Universitatis Upsaliensis

    Författare :Frédéric Haziza; Uppsala universitet.; Uppsala universitet.; [2015]
    Nyckelord :TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; program verification; model checking; parameterized systems; infinite-state systems; reachability; approximation; safety; tree systems; shape analysis; small model properties; view abstraction; monotonic abstraction; Computer Science; Datavetenskap;

    Sammanfattning : This doctoral thesis considers the automatic verification of parameterized systems, i.e. systems with an arbitrary number of communicating components, such as mutual exclusion protocols, cache coherence protocols or heap manipulating programs. The components may be organized in various topologies such as words, multisets, rings, or trees. LÄS MER

  5. 5. Verifying Absence of ∞ Loops in Parameterized Protocols

    Detta är en avhandling från Uppsala : Acta Universitatis Upsaliensis

    Författare :Mayank Saksena; Uppsala universitet.; Uppsala universitet.; [2008]
    Nyckelord :formal methods; verification; model checking; infinite-state systems; regular model checking; liveness; graph transformation;

    Sammanfattning : The complex behavior of computer systems offers many challenges for formal verification. The analysis quickly becomes difficult as the number of participating processes increases.A parameterized system is a family of systems parameterized on a number n, typically representing the number of participating processes. LÄS MER