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.