Program kolokvií s abstrakty pro semestr Jaro 2007
- 20. 2. 2007
- Prof. Rudolf Freund, Technische Universität Wien
- Curricula and Research Topics in "Informatics and Medicine" at the Vienna University of Technology
- Abstrakt: Recognizing the growing importance of computer applications in the areas of medical sciences as well as medical health care, the new curricula in informatics, installing bachelor and master studies at the Vienna University of Technology in 2001, also included a bachelor as well as a master in "Informatics and Medicine". The curricula include the basic courses in computer science and medicine as well as special courses in medical applications. A lot of scientific projects at the Vienna University of technology also include applications in medical health care, e.g., from the visualization of medical data to the development of special equipment for handicapped persons. In the second part of my talk I shall also illustrate current research topics of my group in the area of Natural Computing, especially including results in DNA as well as in Membrane Computing.
- 27. 2. 2007
- Ing. Tomáš Vojnar, Ph.D., FIT VUT, Brno
- Counter Automata in Verification of Programs on Lists or Trees
- Abstrakt:
We first discuss an automated approach for verifying programs
manipulating (possibly cyclic and/or shared) singly-linked lists using
counter automata as accurate models for the programs. Control states
of our counter automata correspond to abstract heap graphs where list
segments without sharing are
collapsed, and counters are used to keep track of the number of
elements in these segments. The technique allows one to verify various
safety properties of the considered programs (as, e.g., absence of
null-pointer dereferences, absence of memory leaks, shape invariance,
preservation of the length of the lists, etc.) as well as termination
of the programs. We also mention a generalisation of the technique
that keeps track of sortedness properties of the lists. In the second
part of the talk, we then introduce a related technique for verifying
tree-manipulating programs. The technique uses abstract regular tree
model checking to obtain invariants of the considered programs (and
check their safety properties). Using the invariants, we build counter
automata simulating the analysed programs and use them to check
termination. We give techniques for automatically refining the
initially obtained counter automata when a spurious lasso-shaped
termination counterexample is witnessed.
These results are a joint work with Ahmed Bouajjani, Peter Habermehl, and Pierre Moro from LIAFA, Paris, Radu Iosif and Marius Bozga from VERIMAG, Grenoble, and Adam Rogalewicz from FIT VUT, Brno.
- 6. 3. 2007
- Prof. Zoltan Esik, University of Szeged
- An algebraic characterization of logics on finite trees
- Abstrakt: Algebraic methods have been very powerful in obtaining *decidable* characterizations of the expressive power of logics on words. For example, every decision procedure for testing first-order definability or definability in Linear Temporal Logic of a regular language is based on testing whether the minimal automaton of the laguage is aperiodic (counter-free). In the talk I will provide an extension of the algebraic methods to logics on trees and provide some applications.
- 13. 3. 2007
- doc. PhDr. Karel Pala, CSc., Mgr. Pavel Rychlý, Ph.D., FIMU, Brno
- Podobnost kontextů ve velkých textových korpusech
- Abstrakt:
Rozsáhlé textové korpusy jsou velice cenným zdrojem informací pro
zpracování přirozeného jazyka, lingvistiku, lexikografii, výuku jazyků
aj. Důležité je vždy zkoumání jednotlivých slov (slovních spojení,
syntaktických struktur) v různých kontextech, protože právě různé
kontexty mají zásadní vliv na význam zkoumaných jevů.
Zmíněny budou metody a techniky rozpoznávání různých typů kontextů a aplikace, které využívají jak jednotlivé kontexty tak podobnost různých kontextů. Dále bude prezentován algoritmus efektivního výpočtu podobností všech dvojic slov na základě statistických charakteristik jednotlivých slov.
- 20. 3. 2007
- doc. Ing. Martin Šperka, PhD., FIIT STU, Bratislava
- Výskum v oblasti vizualizácie a augmented reality na FIIT STU v Bratislave
- Abstrakt: Prehľad projektov z oblasti výskumu nových metód komunikácie človek-počítač s využitím multimédií, vizualizácie, virtuálnej a obohatenej reality a zameraných na rôzne aplikácie s dôrazom na elektronické vyučovanie. Na prednáške budú prezentované niektoré pilotné projekty z hore uvedenej oblasti.
- 21. 3. 2007, B011 14:00
- Dr. Momtchil Peev, Seibersdorf Research, Wien
- Quantum key distribution and (classical) cryptography
- Abstrakt: Quantum key distribution (QKD) is the first real world application of quantum information theory. QKD is on the one hand an essentially quantum technology. Simultaneously it is a (classical) cryptographic primitive which has to be addressed in the broad context of classic cryptography. The relation between QKD and classical cryptography has been recently reviewed in a "White paper: Quantum Key Distribution and Cryptography" by the European Integrated Project SECOQC (http://arxiv.org/abs/quant-ph/0701168). The talk aims at revisiting selected topics from the mentioned recent publication, with an emphasis on the SECOQC-concept of "Network(s) of secrets" and, from the author's perspective, outlines possible future research directions in this field.
- 27. 3. 2007
- doc. RNDr. Antonín Kučera, Ph.D., FIMU, Brno
- Kvantitativní analýza rekurzivních Markovových řetězců
- Abstrakt: Diskrétní Markovovy řetězce jsou obecným modelem systémů, jejichž dynamiku lze charakterizovat pomocí pravděpodobnostních distribucí na přechodech z jednotlivých stavů systému. V přednášce bude podrobněji představena třída rekurzivních Markovových řetězců, která odpovídá pravděpodobnostnímu rozšíření zásobníkových automatů. Během posledních čtyř let byly nalezeny metody, s jejichž pomocí je možné překonat fundamentální obtíže spojené s kvantitativní analýzou těchto řetězců a v některých případech ji provést algoritmicky. Možné aplikace získaných výsledků zahrnují efektivní analýzu rekurzivních náhodnostních algoritmů, návrh alternativních "page-ranking" algoritmů pro internetové vyhledávače a lze je využít i mimo oblast informatiky. Zajímavá je např. souvislost s třídou tzv. vícedruhových náhodnostních procesů s větvením (multitype branching processes), které se hojně využívají v biologii a genetice. Přednáška nepředpokládá znalosti z oblasti teorie stochastických procesů, klíčové pojmy, výsledky a důkazové techniky budou prezentovány ve zjednodušené podobě.
- 3. 4. 2007
- Doc. Dr. Ing. Pavel Zemčík, FIT VUT, Brno
- 2D obrazové klasifikátory, jejich aplikace a akcelerace v DSP a FPGA. 2D Image Classifiers, their application, and acceleration through DSP and FPGA
- Abstrakt:
- Úvod do klasifikace, klasifikace obrazu, spojování slabých klasifikátorů, princip AdaBoost, příznaky užívané ve zpracování obrazu
- Akcelerace AdaBoost v DSP/FPGA, vstupy a výstupy, rozdíly v implementaci extrakce příznaků v software a FPGA
- Aplikace klasifikace obrazu, demonstrace systému pro kontrolu průjezdu na červenou a měření rychlosti se čtením registračních značek pro automobilový provoz
- Introduction in classification, image classification, merging of weak classifiers, AdaBoost principle, features used in image classification
- AdaBoost acceleration in DSP/FPGA, input and output, features, differences in implementation of software and FPGA features
- Applications of image classification, demonstration of system for read light violation and speed measurement system with number plate reading for automotive traffic
- 10. 4. 2007
- prof. PhDr. Eva Hajičová, DrSc., MFF UK, Praha
- Závislostní gramatika a hloubková struktura věty
- Abstrakt:
- Pohled do historie: Popis syntaktických vztahů ve větě chápaných jako vztahy mezi členem řídícím a závislým: Predikát a jeho argumenty, K.F.Becker (1837), německé gramatiky (často s vyčleněním specifického vztahu mezi subjektem a predikátem, podobně u nás Vl. Šmilauer 1947), L. Tesnière (1959, aktanty a cirkumstanty)
- Formální gramatika: Definice, podmínka projektivity – jak se s ní vyrovnat (viz dál, bod 7)
- Srovnání s analýzou na bezprostřední složky (intermediate constituents), frázová gramatika. Problém obdobný neprojektivním konstrukcím: tzv. závislosti na dlouhou vzdálenost (long distance dependencies, unbounded dependencies).
- Od frázové gramatiky přes zavedení hlavních členů („heads“) k závěru, že všechny současné „frázové“ popisy obsahují pojem „head“, tedy členu řídícího (a členů na něm závislých). Otázka: k čemu je třeba členění na fráze?
- Platí: čím blíž má popis k popisu významu, tím důležitější součástí je vztah „predikát a jeho argumenty“, „head“ a „dependents“ nebo podobně (C. Fillmore, J. Robinsonová, lexikálně funkční gramatika). Zdánlivý protipříklad: statistické modely
- AČV jako sémanticky relevantní členění – nevhodnost členění na fráze: pražský Funkční generativní popis, zavedení tzv. pohyblivých složek (floating constituents) v kategoriální gramatice (M. Steedman)
- Jak se vyrovnat v popisu podkladové (hloubkové) struktury s neprojektivitami v povrchové podobě věty: jsou příznakové; ověření teorie na podkladu Pražského závislostního korpusu (PDT)
- 17. 4. 2007
- Prof. Dines Bjorner, TU Lyngby, Dánsko
- Domain Theories and Domain Engineering
- Abstrakt:
Before software can be designed its requirements must be understood. Before equirements can be prescribed the underlying (application) domain must be understood.
These two dogmas unavoidable necessitates that proper, professional software development ideally proceeds in three phases: Domain Engineering (D) ---> Requirements Engineering (R) ---> Software Design (S) whereby correctness of software design is a matter of D, S |-- R, that is, proving that the softwaee, S, meets its requirements, R, in the context of the domain, D. The 'models' relation, |--, formally means that a proof of correctness of S wrt. R often has to rely of explicitly stated assumptions about the domain.
In this seminar we shall primarily talk about Domains - and only indicate how one can safely proceed from a domain description to a requirements prescription.
We shall outline informal and formal approaches to domain descriptions and we shall introduce the model concepts of domain facets: the intrinsic facet, the support technology facet, the management and organisation facet, the rules and regulations (and the derived script) facet, and the human behaviour facet. Throughout we will illustrate with examples taken from such classical domains as transportation (railways) and others.
In "turning" domain descriptions into part of requirements prescrptions we shall hint at such (algebraic) operations as domain projection, domain instantiation, domain determination, domain extension and requirements fitting.
Finally we shall discuss the wider role of Domain Theories and Domain Engineering - while suggesting a wealth of research topics...
- 24. 4. 2007
- Prof. Dalibor Fronček, University of Minnesota Duluth
- Want to schedule an (un)fair tournament?
- Abstrakt:
Suppose you want to schedule a round robin tournament of 8 teams but do
not have enough time to play all 28 games. You may decide that each team
will play just 5 games rather that the usual 7. Now you need to choose
which games to drop. It surely makes a difference if the team ranked No
4 misses the games against the teams ranked No 1 and 2 while team ranked
No 5 misses the games against the teams ranked No 7 and 8. Overall, team
No 5 then has much stronger opponents than No 4.
We will explore ways how to make such a tournament as fair as possible and also how to make it unfair. We will show that these two tasks are in fact complementary and that by achieving one, we also achieve the other. To do that, we introduce some notions of graph theory, including "vertex-magic vertex labeling", and show how graph theory can help us solve the scheduling problem.
- 15. 5. 2007
- Dr. Rudolf Hanka, University of Cambridge
- Content-Based Indexing and Browsing of Medical Images
- Abstrakt: With the rapid growth of digital imaging modalities that are producing a broad spectrum of multimedia data types, medical database management is becoming increasingly complex. How to manage these sophisticated data in a medical image database with the aim of increasing the efficiency of clinical applications is a challenging research issue. The talk will describe the basis of the I-Browse system developed for this purpose at the Medical Informatics Unit in Cambridge.