Rayna Dimitrova
 |
Rayna Dimitrova (Ph.D. Student) Reactive Systems Group |
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. I am currently a research assistant in the DFG SFB/TR 14 Automatic Verification and Analysis of Complex Systems. Previously my research was 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. Synthesis methods start with a formal specification of the system’s behavior, or a partial implementation, and automatically construct an implementation guaranteed to fulfill the specification, or report that the given requirements cannot be realized, if no such implementation exists. A realistic implementation should conform to the interfaces provided for the components in a distributed system, meaning that each component should only depend on the information about its environment that is available via its interface. I develop synthesis methods that respect the interface limitations of the synthesized system components and are applicable to complex, possibly infinite-state, system models. I also aim at advancing formal methods for design and analysis beyond functional correctness, in order to handle fault tolerance and security requirements. My contributions include novel abstraction refinement techniques, synthesis methods and formal specification languages.
Publications
| [DF12] | Rayna Dimitrova and Bernd Finkbeiner. Counterexample-guided Synthesis of Observation Predicates. FORMATS 2012. |
| [DFR12] | Rayna Dimitrova, Bernd Finkbeiner and Markus N. Rabe. Monitoring Temporal Information Flow. ISoLA 2012. |
| [DFKRS12] | Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe and Helmut Seidl. Model Checking Information Flow in Reactive Systems. VMCAI 2012. |
| [DF09] | Rayna Dimitrova and Bernd Finkbeiner. Synthesis of Fault-Tolerant Distributed Systems. ATVA 2009. |
| [DF08] | Rayna Dimitrova and Bernd Finkbeiner. Abstraction Refinement for Games with Incomplete Information. FSTTCS 2008. |
| [DP08] | Rayna Dimitrova and Andreas Podelski. Is Lazy Abstraction a Decision Procedure for Broadcast Protocols? VMCAI 2008. |
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).
Student Projects
| [Dah09] | Daniel Dahrendorf. Symbolic Encodings of Timed Games with Incomplete Information. Master Thesis |