Program kolokvií s abstrakty pro semestr Podzim 2006

26. 9. 2006
doc. Ing. Jan Staudek, CSc., FIMU, Brno
Management informační bezpečnosti (pohled r. 2006 a dál)
Abstrakt: Vybrané mýty a pravdy o informační bezpečnosti, aktuálnost sémantických útoků na informační bezpečnost, dopady masového šíření klasických aplikací v pervasivním síťovém prostředí soudobých mastodontních operačních systémů. Trendy řešení charakterizovatelné systematickým uplatňováním certifikací vůči celosvětově uznávaným standardům, rodina standardů ISO/IEC 27000 a kritéria pro hodnocení informační bezpečnosti (standard ISO/IEC 15408).
3. 10. 2006
Prof. Cristian S. Calude, University of Auckland, New Zealand
Variations on the Halting problem
Abstrakt: The talk deal with several non-traditional approaches to one of the most famous problems of computing: the halting problem for Turing machines.
10. 10. 2006
Prof. RNDr. Jiří Wiedermann, DrSc., Ústav informatiky AV ČR
Chtěli byste být mozkem v baňce?
Abstrakt: Moderní teorie kognitivních systémů pohlíží na tyto systémy jako na roboty - tj. autonomní výpočetní systémy, které jsou vybaveny čidly, jimiž se orientují v prostředí, a manipulátory, pomocí kterých se pohybují v prostředí a vykonávají v něm různé akce. Přesto zejména v kruzích počítačových teoretiků je opakovaně slyšet názory, že na kognici lze pořád možné pohlížet i "klasicky", jako na standardní problém zpracování (byť specifických) dat a že tudíž "vtělení" není nezbytné pro zachycení podstaty kognice. Ukážeme, že takto zjednodušený pohled opomíjí základní vlastnost kognitivních systémů - a sice jejich aktivní vliv na výběr či dokonce vznik vstupních dat. Bez této zpětné vazby si systém nemůže vytvořit svůj vnitřní model světa poznaný prostřednictvím svých akcí. Pro vysvětlení povahy zmíněného problému použijeme výpočetní model kognitivních systémů zavedený autorem. Tento model umožní na principielní úrovni přemýšlet o fungování algoritmických mechanizmů imitace, komunikace, vzniku řeči, myšlení a vědomí a tím přispět i k jejich pochopení v živých systémech.
17. 10. 2006
doc. RNDr. Václav Matyáš, M.Sc., Ph.D., FIMU, Brno
On two experiments in the areas of privacy and security
Abstrakt: First part of this talk introduces results of a study into the value of so-called location privacy for individuals using mobile devices. We questioned a sample of over 1200 people from five EU countries, and used tools from experimental psychology and economics to find out the value that these people attach to their location data. We compare this value across national groups, gender and technical awareness, but also the perceived difference between academic use and commercial exploitation. We provide some analysis of the self-selection bias of such a study, and look further at the valuation of location data over time using data from another experiment.

Second part of my talk presents our experiment of card payment authorisations by both Chip&PIN and handwritten signatures. Introduction of smartcards within the Chip&PIN deployment exercise is quite likely the most extensive deployment of computers in the human history, with security as a major aspect. Our experiment attempted to find out whether customers truly benefit from the Chip&PIN introduction with respect to an opportunistic thief. This is, to our best knowledge, the first presentation of non-trivial field experiment results on the ease of PIN in-shop observation to the general public worldwide.

24. 10. 2006
Prof. Dr. Pavel Materna, CSc., Doc. RNDr. Marie Duží, CSc., FF MUNI Brno, VŠB Ostrava
Transparentní intensionální logika a pravidlo β-redukce
Abstrakt: Transparentní intensionální logika (TIL) může být po formální stránce považována za hyper-intensionální λ-kalkul pracující s parciálními funkcemi. Termínem „hyper-intensionální“ zde míníme to, že termy λ-kalkulu nejsou interpretovány jako funkce (tj. množinová zobrazení), nýbrž jako procedury, jejichž výstupem jsou označené funkce. Navíc, zmíněné procedury, známé jako TIL konstrukce, jsou objekty sui generis, mohou být tedy v rámci teorie nejen užívány, ale také zmiňovány. Přitom TIL pracuje s parciálními funkcemi a z teorie λ-kalkulu je známo, že při práci s parciálními funkcemi β-redukce není obecně korektním pravidlem. Problém spočívá v tom, že k tomu, aby byla substituce korektní i v (hyper-)intensionálních kontextech, nestačí zabránit kolizi proměnných. Jelikož však je pravidlo β-redukce základním výpočtovým pravidlem, bez kterého se při práci s λ-kalkulem neobejdeme, ukážeme v přednášce, jak β-redukci definovat a korektně používat i v tak bohatém aparátu, jakým je TIL. Využijeme techniky, která je v programování známa jako „předávání parametru hodnotou“ a nemá vedlejší efekty, na rozdíl od „předávání parametru jménem či odkazem“.
31. 10. 2006
Dr. Martin Rayman, EPFL Center for Global Computing, TU Lausanne
P2P Information Retrieval from the Web
Abstrakt: Web search over peer-to-peer (P2P) networks shows promise to become an alternative to the state-of-the-art search engines since P2P overlays offer means for decentralized search across widely-distributed document collections. However, the design of effective techniques for P2P indexing and retrieval raises a number of technical challenges due to potentially unscalable resource (e.g. bandwidth, storage) consumption.

In this presentation, we will present a framework for full-text information retrieval in structured P2P networks and introduce a novel retrieval model based on highly discriminative keys - terms and term sets appearing in a restricted number of documents - that ensure efficient and scalable retrieval. Our goal is to design scalable techniques for building a global key index in structured P2P overlays for large document collections. We present experimental results that show acceptable indexing and retrieval costs while the retrieval quality is comparable to standard centralized solutions with state-of-the-art ranking.

7. 11. 2006
doc. RNDr. Lubomír Popelínský, Ph.D., FIMU, Brno
On Czech text classification
Abstrakt: Text classification - automatically classifying documents into one of predefined classes by means of machine learning - is one of the most successful applications of text mining. Text classification can be typically used for authorship, genre/source or topic recognition. We start with discussing excellent results that have been achieved for classification of English documents.

For highly inflective languages like Czech the task is supposed to involve additional effort. Pre-processing steps - lemmatization, feature (important word) selection, shallow parsing - can be important factors in classifying Czech texts. The articles used in these experiments had been taken from Czech newspapers. Several tasks concerned authorship recognition, the other to find a document source - either a newspaper or a particular page (or column). Topic recognition was the goal of two tasks.

We also introduce two novel methods of text categorization in which documents - English, French and Czech.- are split into fragments.

14. 11. 2006
prof. Ing. Miroslav Švéda, CSc., FIT VUT, Brno
A Design Framework for Internet-Based Embedded Distributed Systems
Abstrakt: This paper presents concepts of a specification-driven design framework aiming at IEEE 1451-based embedded distributed systems that consist of smart components connected to Internet. It deals with an integrated networking approach based on the IEEE 1451.1 object-based networking model, which is complemented by the Internet Protocol (IP) multicast that mediates efficient and unified access from Internet to distributed components. The kernel of the paper deals with tools and techniques aiming to prop specification and design life cycle phases of applications under development.

The presented, incrementally developed design framework stems from verifiable formal specifications as a launching paradigm, from Internet-based distributed HW/SW components with IP multicast as an architectural paradigm, and from reusability paradigm supporting design process from specification to implementation and testing.

21. 11. 2006
Mgr. Michal Kunc, Ph.D., PřF MU, Brno
Co víme o jazykových rovnicích?
Abstrakt: Přestože algebry jazyků s operací zřetězení (a případně i s Booleovskými operacemi, Kleeneho hvězdičkou a jinými) jsou jedním z nejdůležitějších objektů teoretické informatiky, jejich základní algebraické vlastnosti nebyly dosud dostatečně pochopeny. Mimo jiné, donedávna nebylo známo téměř nic o chování ani nejjednodušších rovnic v těchto algebrách. Jedinou výjimkou jsou explicitní systémy jazykových rovnic, které však byly obvykle používány pouze jako výhodný způsob zápisu bezkontextových jazyků, a jejich potenciál popisovat jiné zajímavé třídy jazyků byl přehlížen. Na druhou stranu, s implicitními jazykovými rovnicemi, kde jedinou operací je zřetězení, se setkáváme jako s přirozeným zobecněním již dlouho intenzivně studovaných rovnic na slovech. Ale přestože pro rovnice na slovech jsou známy mnohé hluboké výsledky (například algoritmy pro rozhodování řešitelnosti), tyto výsledky není možné zobecnit na případ rovnic jazykových (existence řešení není rozhodnutelná již pro velmi jednoduché jazykové rovnice).

V přednášce zmíníme některá známá elegantní použití jazykových rovnic k důkazu základních tvrzení o formálních jazycích, a poté předvedeme nejnovější výsledky o vyjadřovací síle a řešitelnosti různých typů systémů jazykových rovnic.

28. 11. 2006
Prof. Dr. Ralf H. Reussner, Universität Karlsruhe
Components beyon Black boxes - Architectural Analysis with Parametric Component Contracts
Abstrakt: This talk discusses the role of software components for an engineering approach to software construction. In particular, this talk concentrates on predicting functional and extra-functional properties of layered component-based software architectures. The approach presented is based on parametric contracts, a generalisation of design-by-contract.

Firstly, the talks discusses the role of component-based software engineering plays for software engineering in general. Secondly, we adresses the meaning of the "contractual use of components", a term sometimes used loosely - or even inconsistently - in current literature. Thirdly, we introduce the abstract concept of parametric contracts. It is shown how parameterised contracts are used to compute the properties of a component in dependence from its environment. We sketch algorithms for computing a component's IDL-style interfaces, protocols and its services' reliabilites and response time.

5. 12. 2006
Ing. Július Štuller, CSc., Ústav informatiky AV ČR
Aktuálne trendy v oblasti semantického webu
Abstrakt: Vizie semantickeho webu sa nenaplnaju tak rychle, a ani lahko, ako mnohi - vratane ich tvorcov - predpokladali a ocakavali. Polovicka dekady existencie myslenky semantickeho webu dovoluje sa kriticky ohliadnut za dosiahnutymi vysledkami a triezvejsie odhadnut povodnu realnost atraktivnych vizii semantickeho webu. Prednaska sa zameria na hlavne aktualne trendy v tejto oblasti i na mozne priciny nenaplnenych ocakavani, a to ako v oblasti teoretickej, tak i praktickej.
12. 12. 2006
Mgr. Jan Kasprzak, FIMU, Brno
Spam včera, dnes, a bohužel i zítra
Abstrakt: Jak fungování elektronické pošty usnadňuje život spammerům a tím jej znesnadňuje obyčejným lidem. Co je spam, odkud se bere, jaké má vlastnosti. Jak spam rozpoznat a efektivně se mu bránit. Jak tyto obrany lze obejít a proč tady spam bude nejspíš stále. Doporučené praktiky pro konfiguraci poštovních serverů se zaměřením na snížení množství smetí v elektronické poště.
19. 12. 2006
Dr. Jaco van de Pol, CWI Amsterdam
Symbolic and Algorithmic Techniques for the Verification of Large Distributed Systems
Abstrakt: In order to model the behaviour of large distributed systems, one should focus on the interaction between components. However, for realistic systems it is also important that various data structures can be modelled. To this end, we use a combination of process algebra and abstract data types, called muCRL.

Verifying such systems can be done either by proving equivalence between a system's specification and implementation, or by verifying temporal properties of the implementation. We typically work in a branching time setting, i.e. bisimulation as the equivalence, and mu-calculus as temporal logic.

Model checking is a powerful algorithm to verify the correctness of distributed systems, but suffers from the so-called state explosion. Several techniques have been developed to overcome this problem. This talk will mainly focus on the detection and deployment of confluence (a branching-time variant of partial-order reduction). Here automated theorem proving techniques are used to prune the state space for the model checker.

If time permits, I will also provide a short overview of our work on distributed state space generation and reduction modulo bisimulation.