Rayna Dimitrova

Rayna Dimitrova (Ph.D. Student) Reactive Systems Group Universität des Saarlandes Phone: +49 681 302 5620 Fax: +49 681 302 5636 eMail: dimitrova at cs.uni-sb.de Building: E 1 3 Room: 507

About me

I am a Ph.D. student in the Reactive Systems Group in the Computer Science Department at Saarland University under the supervision of Prof. Bernd Finkbeiner. My research is supported by a scholarship from Microsoft Research Cambridge.

Research

The need for rigorous techniques for verifying complex software systems is well understood. Since the cost of repairing an error grows dramatically with the stage of the development the error is found in, it is imperative to verify the system as early as possible. My goal is to develop verification techniques that are already applicable to partial designs. In particular, the focus of my work is the analysis of incomplete information, which is a major concern in partial-design verification and synthesis of distributed systems, as individual components have only partial view on the global state of the system.

The partial-design verification problem can be reduced to the problem of solving an infinite game under incomplete information. The game is between the team of components for which there is no implementation yet (and whose objective is to guarantee correct system behavior) and the team of the components for which implementation is available, together with the external system environment (whose objective is to exhibit an error). The challenge to extend existing algorithms for solving such games to software systems lies in the fact that software typically operates on variables whose domains are infinite, such as integers, unbounded message queues, etc, i.e, it is necessary to consider models with infinite state-spaces. In order to meet this challenge, we have proposed an abstraction-refinement procedure for two-player safety games with incomplete information.

Fault-tolerance, i.e., the ability of a system to withstand situations where a subset of its components breaks, is an important design consideration in distributed systems and is also a major source of incomplete information, since faults affect the communication between processes and hence also the information the non-faulty processes have. We developed a synthesis algorithm that determines if a given external CTL* specification has a fault-tolerant implementation for a fully-connected system architecture, and, in case the answer is positive, automatically derives such an implementation. Thus, we established that in this case the fault-tolerant synthesis problem is decidable and, in fact, no more expensive than standard synthesis.

Publications

Teaching

• Seminar Games in Verification and Synthesis (SS 08) In this seminar, we will study game-theoretic methods that derive implementations from formal specifications (synthesis) and that prove that a given implementation satisfies a logical property (verification). In both cases, we view the interaction between a software component and its environment as an infinite game; verification then amounts to checking that the strategy represented by the program is winning; synthesis amounts to deriving a winning strategy from a logical description of the winning condition.
• Teaching Assistant in lecture Verification (WS 07/08) This course gives an introduction to various fields of systems verification, with an emphasis on algorithmic verification (model checking) and deductive verification (theorem proving).

Recent Student Projects