Projects

Model Checking

Model checking gives us an algorithmic means to determine whether an abstract model, which represents, for example, a Java program, satisfies a property expressed in a particular logic. In case the property is not satisfied, it identifies a counterexample that shows why the property does not hold.

Lock-Free Algorithms

In distributed systems where many processes access shared data, locks are often used to ensure that processes cannot simultaneously perform updates on the same part of the data. This approach has disadvantages: lack of fault-tolerance, fast processes having to wait for slower ones, and reduced parallelism. Lock-free algorithms avoid these problems while maintaining data consistency. The groups work on this project is done in collaboration with researchers from EPFL, the Technion, the University of Crete and the University of Toronto.

Population Protocols

Population protocols emerged in 2004 as a new theoretical model for describing mobile systems in which the components have sharply limited computational power. The model makes minimal assumptions about many aspects of the system, with the goal of making the model widely applicable, but also tractable for theoretical analysis. Our work on this model has been done in collaboration with researchers from EPFL, Université Paris 7 and Yale University.

Quantitative Verification

The majority of the verification methods for concurrent systems only produce qualitative information. Questions like ``Does the system satisfy a particular property?'' and ``Do the systems behave the same?'' are answered. However, for systems that depend on quantitative information such as time and probabilities, answers to these yes-no questions are of little value. Small changes to the quantitative information, which is often obtained experimentally and, hence, is just an approximation, may change the answer from yes to no or vice versa.