Sökning: "decidability"

Visar resultat 1 - 5 av 13 avhandlingar innehållade ordet decidability.

1. 1. Verification of networks of communicating processes : Reachability problems and decidability issues

   Författare :Othmane Rezine; Parosh Aziz Abdulla; Mohamed Faouzi Atig; Bengt Jonsson; Barbara König; Uppsala universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; program verification; model checking; infinite-state systems; distributed programs; concurrent programs; networks of communicating processes; reachability; termination; decidability; Computer Science; Datavetenskap;

   Sammanfattning : Computer systems are used in almost all aspects of our lives and our dependency on them keeps on increasing. When computer systems are used to handle critical tasks, any software failure can cause severe human and/or material losses. LÄS MER

3. 2. Model Checking Parameterized Timed Systems

   Författare :Pritha Mahata; Parosh Abdulla; Jean-Francois Raskin; Uppsala universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Model Checking; Parameterized Systems; Undecidability; Timed Petri Nets; Timed Networks; Computer science; Datavetenskap;

   Sammanfattning : In recent years, there has been much advancement in the area of verification of infinite-state systems. A system can have an infinite state-space due to unbounded data structures such as counters, clocks, stacks, queues, etc. It may also be infinite-state due to parameterization, i.e. LÄS MER

4. 3. On Simultaneous Rigid E-Unification

   Författare :Margus Veanes; Andrei Voronkov; Uppsala universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Datalogi; Computing Science;

   Sammanfattning : Automated theorem proving methods in classical logic with equality that are based on the Herbrand theorem, reduce to a problem called Simultaneous Rigid E-Unification, or SREU for short. Recent developments show that SREU has also close connections with intuitionistic logic with equality, second-order unification, some combinatorial problems and finite tree automata. LÄS MER

5. 4. Logics of Knowledge and Cryptography : Completeness and Expressiveness

   Författare :Mika Cohen; Mads Dam; Alessio Lomuscio; KTH; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; epistemic logic; first-order logic; formal cryptography; static equivalence; security protocols; BAN logic; multi-agent system; completeness; logical omniscience problem; Computer science; Datavetenskap;

   Sammanfattning : An understanding of cryptographic protocols requires that we examine the knowledge of protocol participants and adversaries: When a participant receives a message, does she know who sent it? Does she know that the message is fresh, and not merely a replay of some old message? Does a network spy know who is talking to whom? This thesis studies logics of knowledge and cryptography. Specifically, the thesis addresses the problem of how to make the concept of knowledge reflect feasible computability within a Kripke-style semantics. LÄS MER

7. 5. 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