J. Hollmen, J. K. Seppänen, and H. Mannila. Mixture models and frequent sets: combining global and local methods for 0-1 data. Proc. of 3rd SIAM Int. Conf. on Data Mining, pp. 289-293. SIAM, 2003. [pdf]
Abstract: In the talk, I will describe some recent research in data analysis of high-dimensional discrete data. Some practical uses of binary (0-1) data representations are given and some general methodologies analyzing 0-1 data are reviewed. Two traditions - global and local methods - of data mining in the context of binary data are described and some of our research work on combining these two traditions using mixture models and frequent sets are presented.
M. Pentus, Lambek calculus is NP-complete, CUNY Ph.D. Program in Computer Science Technical Report TR-2003005, CUNY Graduate Center, New York, May 2003. [pdf]
Loengukonspekt. [pdf]
Ettekande slaidid. [pdf]
Abstract: A formal language is a (usually infinite) set of finite words over a finite alphabet. In late 1950s J. Lambek proposed a logico-algebraic approach to formal language specification (as opposed to Chomsky's recursion-theoretic approach). In Lambek's approach a formal language (e.g. an approximation of a natural language or a programming language) is specified by a grammar which consists of 1) a finite binary relation that assigns types (involving multiplication, left and right division) to the elements of the alphabet and 2) a fixed calculus for deriving reduction laws of the types. This calculus, now called the Lambek calculus, is one and the same for all Lambek grammars. It has turned out that Lambek grammars yield exactly the class of context-free languages.
The Lambek calculus can be easily embedded into multiplicative noncommutative linear logic, for which the derivability problem is clearly in NP. We show that in fact the problem is NP-complete and that moreover the derivability problem for the Lambek calculus is NP-complete.
Ettekande slaidid. [pdf]
Kokkuvõte:Juba eelmise sajandi 80te aastate lõpuks oldi jõutud arvutustehnilise riistvara projekteerimise automatiseerimisel nii kaugele, et süsteemi kirjeldamiseks piisas loogikafunktsioonidest. Ülejäänuga, st. funktsioonide teisendamise loogikaelementide skeemiks ja nende elementide paigutamisega ränikristalli pinnale (või trükiplaadile), saab üliedukalt hakkama arvutiprogramm. Sarnaselt tarkvara projekteerimisega, kus oli juba toimunud üleminek assemblerkeeltelt kõrgtasemekeeltele, hakati ka riistvara projekteerimisel üha rohkem rääkima ränikompilaatoritest - vahenditest, mille sisendiks oleks kõrgtasemekeeles kirjeldatud algoritm ja väljundiks skeem loogikaelementidest.
Kuni 90te aastate keskpaigani toimus tormiline ja paljulubav areng, sest signaalitöötlusalgoritmide puhul saab väga edukalt kasutada tarkvarakompilaatorite arendamise ja projekteerimise kogemusi. Samuti on võrreldav mõlema ülesande keerukus. Sellest ajast on pärit ka enamlevinumad nimetused - kõrgtasemesüntees ja käitumuslik süntees. Edasi järgnes aga seisak, sest mitte kõik riistvaras realiseeritavad algoritmid ei tegele numbrilise signaalitöötlusega. Peamiseks põhjuseks on riistvara kompileerimise ülesande üldjuhu oluliselt suurem keerukus. Kõige olulisemana võiks välja tuua teguri, mida tarkvara kompileerimisel pole enamasti vaja üldse arvestada - riistvaraline arhitektuur pole üldjuhul fikseeritud. See tähendab, et eksisteerib praktiliselt piiramatu arv võimalusi arvutuslike sõlmede, ühendussiinide ja mäluelementide omavahelisteks ühendusteks.
Praegusel ajal on kõrgtaseme sünteesi areng faasis, kus integreeritakse erinevat tüüpi algoritmide kompileerimiseks vajalikke lähenemisi. Ühtlasi toimub ideede vahetamine tark- ja riistvara kompileerimistehnikate vahel, sest paljud alamülesanded on sarnased. Sarnaselt riistvaraga on kaasaegsed protsessorid suutelised täitma mitut üksikkäsku (operatsiooni) korraga. Samuti on sarnased andme- ja kontrollvoo kujutamise ja optimeerimise vahendid. Isegi kõrgtaseme sünteesi üksiksammud on võrreldavad osade tarkvara kompileerimise sammudega:
Ettekande slaidid. [pdf]
Kokkuvõte: Andmekaevandamise üks olulisi meetodeid on klasterdamine, mille käigus jagatakse andmeobjektid sarnasuse alusel gruppidesse. Seejuures tekib küsimus, mitmesse gruppi peaks andmed jagama. Hierarhiline klasterdamine lahendab selle küsimuse nii, et leiab klasterduste hierarhia, mille järgi saab hõlpsasti leida klasterdused iga võimaliku gruppide arvu jaoks. Paraku võib suure arvu andmeobjektide korral hierarhilise klasterduse esimese sammuna tehtav kõikide andmeobjektide vaheliste sarnasuste mõõtmine olla liiga aeglane. Ettekandes on vaatluse all meetod, mis väldib selliste kauguste mõõtmist, mille kohta saab kolmnurgavõrratust kasutades järeldada, et tegemist on teineteisest kaugete objektidega. Seejärel tuleb veel teostada klasterdamine osalise informatsiooni alusel, tulemuseks on ligikaudne hierarhiline klasterdus.
Ettekande slaidid. [pdf]
Kokkuvõte: E-äri protokollidel/protokollistikel on tihtipeale turvanõudeid, mida "tavalistel" krüptoprotokollidel ei ole. Need täiendavad turvanõuded puudutavad enamjaolt salgamise vääramist, st. kui üks osapool teisele midagi ütleb, siis tahab teine kindel olla, et ta suudab edaspidi tõestada, et esimene osapool seda ütles.
Ettekandes esitame aksiomaatilise süsteemi, mis on sobilik selliste omaduste üle arutlemiseks, samuti anname sellele süsteemile semantika. Varemesitatud süsteemidest erineb meie oma selle poolest, et selgelt on eraldatud see, mida mingi agent teab ning see, mida ta usub. Ka on semantikas defineeritud, kuidas millessegi uskumine kujuneb. Selline eraldatus lubab meil arutleda ka juhtude üle, kus mõni usaldatud osapool valetab. Usaldatud osapoolel valetamise lubamine on oluline juhtudel, kus me tahame piirata, kui palju me seda osapoolt ikka usaldama peame. Teine täiendus meie süsteemis on modaalsus "agent P suudab teha nii, et valem A kehtib". See modaalsus lubab peale salgamise vääramise ("P suudab Qle tõestada, et A" on avaldatav kujul "P suudab teha nii, et Q usub, et A") väljendada veel teisigi mõistlikke omadusi, näiteks seda, et üks osapool suudab kontrollida, et mõni teine osapool korrektselt oma protokolli täidab.
Kokkuvõte: Igaüks meist on kasutanud ligikaudset otsingut alates Google'i päringutest ning lõpetades inglise-eesti sõnastikuga. Ligikaudse päringu korral defineeritakse objektide erinevust iseloomustav kaugusmõõt ning vastuseks on kõige lähem(ad) kirje(d).
Üha rohkem kogutakse poolavalikke andmeid, mille avaldamine on ebasoovitav või majanduslikult kahjulik. Kuid samas on andmeid vaja kasutada ning müüa. Ka päring võib olla kompromiteeriv. Päring võib sisaldada (varjatult) delikaatseid andmeid või paljastada plaane. Ideaalis peaks küsija saama vaid vastuse ning vastaja jääma õndsasse teadmatusse.
Nii Yao kui Goldreich'i poolt loodud üldised lahendused kindlustavad iga "mõistliku" arvutuse turvalisuse, kuid samas on lahendused siiski liiga ebaefektiivsed. Nii on lootust leida efektiivsem potokoll ka ligikaudsele otsingule.
Ettekandes analüüsime Du ja Attallah' pakutud ligigaudse otsingu protokollide turvalisust, võimalikke ründeid ning pakume välja omapoolseid lahendusi. Lisaks toome eraldi välja mõned üldisemad tulemused. Ettekande aluseks minu ja Helger Lipmaa ühine töö.
H. Lipmaa. On Diophantine Complexity and Statistical Zero-Knowledge Arguments. In C. S. Laih, ed, Advances on Cryptology - ASIACRYPT 2003 (Taipei, Taiwan, 30 Nov.-4 Dec. 2003), v. ? of Lecture Notes in Computer Science, pp. ?-?. Springer-Verlag, Berlin, 2003. [ps.gz]
Ettekande slaidid. [pdf]
Abstract: We show how to construct laconic honest-verifier statistical zero-knowledge Diophantine arguments of knowledge (HVSZK AoK) that a committed tuple of integers belongs to $S$ for all languages in bounded arithmetic. While doing this, we propose a new algorithm for computing the Lagrange representation of nonnegative integers and a new efficient representing polynomial for the exponential relation. As applications, we construct the most efficient known HVSZK AoK for nonnegativity, the first constant-round laconic HVSZK AoK for exponential relation, and propose communication-efficient versions of the Damgård-Jurik multi-candidate voting scheme and of the Lipmaa-Asokan-Niemi $(b+1)$st-price auction scheme.
Ettekande slaidid. [pdf]
Kokkuvõte: Programmi slitseerimine on üks programmianalüüsi konkreetseid rakendusi. Siin on ülesandeks leida antud programmi ja nn slitseerimiskriteeriumi järgi programmi alamhulk, mis on kriteeriumi suhtes relevantne, ehk sliits.
Ettekanne tutvustab erinevaid viise sliitsi täpseks defineerimiseks ning erinevaid lähenemisi programmide automaatsele slitseerimisele.
Ettekande slaidid. [pdf]
Abstract: We present a framework for creating visual specification-languages, where the visual specification could be directly translated into executable code. The approach taken is similar to the one implemented in the NUT system. In the suggested framework, the visual language is designed (compositionally) on top of a set of annotated Java classes, where the annotations are pre- and postconditions stating the possible computational usage of classes and their methods, so that the classes could be used in program synthesis. The talk will give a very brief overview of automated composition of Java-software, the specification language used, and then concentrate on presenting a demo of the implemented framework.
Ettekande slaidid. [pdf]
Kokkuvõte: Käesoleva töö tulemusena loodi uus Linux/Windows keskkonnas kasutatav tarkvaratoode modulaarsel aritmeetikal põhineva avaliku võtme krüptograafia õpetamiseks. Projektiga püüti täita tühimikku avalikul võtmel baseeruva krüptograafia õpiprogrammide valdkonnas.
TECP on keskkonnaks, kus saab luua avaliku võtme krüptograafial baseeruvaid protokolle ning testida nende tööd. Keskkond võimaldab järgnevat:
Ettekande slaidid. [pdf]
Kokkuvõte: Sardsüsteeme on projekteeritud aastakümneid ja alati on sisulise töö ees seisnud lahendusest sõltumatu probleemi püstitus. Tunnetus, et süsteemi silma järgi lõikumine riist- ja tarkvaraks on ääretult ebausaldusväärne, kujunes alles pikkamööda ja teravnes järsult koos integratsiooniastme tõusuga. Termin koosdisain on pärit 90te algusest ja sellega kaasnes hulga arvutiteadlaste teravdatud huvi probleemi vastu, andes tulemuseks nii puht-teoreetilisi käsitlusi kui ka praktilisi projekteerimissüsteemidesse integreeritud algoritme. 90te lõpus tekkinud uus termin süsteemide (kiipsüsteemide, kiipvõrksüsteemide) süntees on neelanud enda alla kunagise koosdisaini paradigma, aga tehnoloogia areng on lisanud ülesandesse järjest uusi mõõtmeid nagu energiatarve, tõrkekindlus, testitavus, uued segatehnoloogiad jne. On see vaid kvantitatiivne muutus või on siin tegemist täiesti uue paradigmaga?
Kõige selle taga on üllatavalt tuttavad graafitöötluse ja optimiseerimisalgoritmid, raskuspunktiks on vaid lähteandmete skaleerimine, erijuhtumite arvestamine, tulemuste interpreteerimine ja kõige selle integreerimine toimivate kõrge intellektuaalse pärandiga riist- või tarkvara arendussüsteemide juurde.
Kokkuvõte: Suuremaid elektroonikasüsteeme projekteeritakse reeglina spetsiaalsetes kõrgtaseme keeltes, millest üks on VHDL. Taoliste spetsifikatsioonide detailne kontrollimine ja parandamine enne spetsifikatsiooni teisendamist tegelikuks riistvaraks on reeglina hädavajalik.
Kaks põhimeetodit spetsifikatsiooni kontrolliks on: 1) Süsteemi simuleerimine arendaja poolt, 2) automatiseeritud tõestused spetsifikatsiooni vastavusest või mittevastavusest hulgale arendaja poolt ettepandud nõuetele.
Praktikas kasutatakse taoliste tõestuste ja, vastupidi, mittekorrektsuse näitamise jaoks enamasti lausearvutusel põhinevaid meetodeid. Paraku osutuvad mõningat tüüpi nõuded ja spetsifikatsioonid lausearvutuse jaoks kas ülemäära keerulisteks või ei ole lausearvutuse abil võimalik kõiki nõudeid/spetsifikatsioone adekvaatselt esitada. Koostöös rootsi ettevõttega SafeLogic ja Chalmersi Tehnikaülikooliga oleme arendanud süsteemi, mis võimaldab klassikalise esimest järku predikaatarvutuse tõestajate kasutamist süsteemide automaatseks verifitseerimiseks. Ettekandes anname ülevaate teostatud uurimustest, eksperimentidest ja rakendustest, samuti vajalikust infrastruktuurist taoliste süsteemide kasutamisel.
Enn Tõugu ettekande konspekt. [doc]
Jaan Penjami ettekande slaidid. [pdf]
T. Altenkirch, T. Uustalu. Normalization by evaluation for $\lambda^{\rightarrow 2}$. Submitted. [ps.gz]
Ettekande slaidid. [pdf]
Kokkuvõte: Otsustuspuid kasutava väärtustusfunktsiooni pöördfunktsiooni konstruktsiooni abil näitame, et hulgateoreetiline semantika on Bool-tüübiga (kuid tüübimuutujateta) lihtsalt tüübitud lambda-arvutuse jaoks täielik. Ühtlasi saame programmi lambda-termide normaliseerimiseks väärtustamise kaudu hulgateoreetilises semantikas. Konstruktsiooni korrektsuse tõestus kasutab loogiliste relatsioonide tehnikat. (Ühistöö Thorsten Altenkirchiga.)
Ettekande slaidid. [pdf]
Kokkuvõte: Teaduslikes arvutustes kasutatakse suurte lineaarsete võrrandisüsteemide lahendamiseks tihti iteratiivseid meetodeid kus lahendit otsitakse nn. Krõlovi alamruumis. Ettekandes anname lühikese ülevaate sellistest meetoditest. Seejärel arutleme teemal - miks ja kuidas kõige efektiivsemalt antud meetodeid realiseerida paralleelarvutitel, milliseid probleeme esineb ning kuidas neid ületada.
Ettekande slaidid. [pdf]
Kokkuvõte: Üks raskemaid probleeme tavavalimiste asendamisel e-valimistega on häälte salajasuse tagamine. Ühest küljest tuleb hääled kaitsmata sidekanalites ülekandmise tarvis krüptida, teisest küljest aga peab keegi suutma antud hääled üle lugeda. See tähendab, et keegi peab valdama hääle dekrüptimiseks vajalikke võtmeid. Praktikas üritatakse neid võtmeid reeglina hajutada erinevate serverite vahel, kuid põhimõtteliselt on nende serverite koostöö tulemusena võimalik kõigi üksikhäälte väärtused välja selgitada. Ettekandes uurime, kas ja millise ülesandepüstituse korral on võimalik privaatsuse tagamisel paremaid tulemusi saavutada.
Ettekande slaidid. [pdf]
Abstract: tba.
Ettekande slaidid. [pdf]
Abstract: When trying to apply Data Flow Frameworks to the analysis of complicated qualities of computer programs, one has to handle the problem of infinite property domains. In such nasty domains, which usually contain infinite ascending chains, fix-point calculations are not guaranteed to terminate.
A common approach is to approximate that domain with a finite abstract domain using Galois connections. However, there is another method, which is more powerful. One can use widenings to enable the fix-point calculation to terminate and narrowings to fine-tune the result. It can be shown that this method is more general than the Galois connection approach.
Although this presentation will be a tutorial/introductory talk with many illustrations, some familiarity with the concept of abstract flowers (or simply program analysis) will greatly enhance understanding. In addition to illustrative text-book examples, we will see how this approach has been used in real life, both in Data Flow Analysis and in Model Checking.
Helger Lipmaa