Sökning: "Parosh Aziz Abdulla"

Visar resultat 1 - 5 av 8 avhandlingar innehållade orden Parosh Aziz Abdulla.

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

   Författare :Frédéric Haziza; Parosh Aziz Abdulla; Tomáš Vojnar; Uppsala universitet; []
   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

3. 2. Reduction Techniques for Finite (Tree) Automata

   Författare :Lisa Kaati; Parosh Aziz Abdulla; Frank Drewes; Uppsala universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Finite automata; tree automata; bisimulation; minimization; simulation; composed bisimulation; composed simulation; Datavetenskap; Computer Science;

   Sammanfattning : Finite automata appear in almost every branch of computer science, for example in model checking, in natural language processing and in database theory. In many applications where finite automata occur, it is highly desirable to deal with automata that are as small as possible, in order to save memory as well as excecution time. LÄS MER

4. 3. 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

5. 4. Verification of Software under Relaxed Memory

   Författare :Carl Leonardsson; Bengt Jonsson; Parosh Aziz Abdulla; Mohamed Faouzi Atig; Viktor Vafeiadis; Uppsala universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; verification; relaxed memory models; Datavetenskap; Computer Science;

   Sammanfattning : The work covered in this thesis concerns automatic analysis of correctness of parallel programs running under relaxed memory models.When a parallel program is compiled and executed on a modern architecture, various optimizations may cause it to behave in unexpected ways. LÄS MER

7. 5. Model Checking of Software Systems under Weak Memory Models

   Författare :Tuan-Phong Ngo; Mohamed Faouzi Atig; Parosh Aziz Abdulla; Philipp Rümmer; Viktor Vafeiadis; Uppsala universitet; []
   Nyckelord :TEKNIK OCH TEKNOLOGIER; ENGINEERING AND TECHNOLOGY; Model checking; Concurrent program; Weak memory model; Computer Science; Datavetenskap;

   Sammanfattning : When a program is compiled and run on a modern architecture, different optimizations may be applied to gain in efficiency. In particular, the access operations (e.g., read and write) to the shared memory may be performed in an out-of-order manner, i. LÄS MER