Sökning: "bisimulation"

Visar resultat 11 - 15 av 16 avhandlingar innehållade ordet bisimulation.

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

    Författare :Mats Kindahl; Parosh Aziz Abdulla; Uppsala universitet; []
    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

  3. 12. The Fusion Calculus : Expressiveness and Symmetry in Mobile Processes

    Författare :Björn Victor; Joachim Parrow; Uppsala universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Computer Systems; Datorteknik;

    Sammanfattning : The fusion calculus is presented as a significant step towards a canonical calculus of concurrency. It simplifies and extends the π-calculus of Milner, Parrow and Walker.The fusion calculus contains the polyadic π-calculus as a proper subcalculus and thus inherits all its expressive power. LÄS MER

  4. 13. Culling Concurrency Theory : Reusable and trustworthy meta-theory, proof techniques and separation results

    Författare :Johannes Åman Pohjola; Joachim Parrow; Björn Victor; Uwe Nestmann; Uppsala universitet; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Computer Science; Datavetenskap;

    Sammanfattning : As concurrent systems become ever more complex and ever more ubiquitous, the need to understand and verify them grows ever larger. For this we need formal modelling languages that are well understood, with rigorously verified foundations and proof techniques, applicable to a wide variety of concurrent systems. LÄS MER

  5. 14. Equivalences and Calculi for Formal Verification of Cryptographic Protocols

    Författare :Johannes Borgström; Uwe Nestmann; Thomas A Henzinger; Martin Odersky; Andrew D Gordon; Viktor Kuncak; Björn Victor; EPFL; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES;

    Sammanfattning : Security protocols are essential to the proper functioning of any distributed system running over an insecure network but often have flaws that can be exploited even without breaking the cryptography. Formal cryptography, the assumption that the cryptographic primitives are flawless, facilitates the construction of formal models and verification tools. LÄS MER

  7. 15. Towards a Trustworthy Stack: Formal Verification of Low-Level Hardware and Software

    Författare :Ning Dong; Roberto Guanciale; Mads Dam; Magnus Myreen; KTH; []
    Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Formal Verification; Information Flow; Refinement; Interactive Theorem Prover; HOL4; Serial Interface; Pipelined Processor; Microarchitecture; Out-of-order Execution; Formell Verifiering; Informationsflöde; Förfining; Interaktiva Bevisprogrammet; HOL4; Seriellt Gränssnitt; Pipelined Processor; Mikroarkitektur; Omordnad Exekvering; Datalogi; Computer Science;

    Sammanfattning : Computer systems, consisting of hardware and software, have gained significant importance in the digitalised world. These computer systems rely on critical components to provide core functionalities and handle sensitive data. LÄS MER