Upp till webbsidan för doktorandseminarierna.
Syftet med seminariet är att ge litet grand av en känsla för vad beviskomplexitet är och hur satser och bevis inom området kan se ut. Den huvudsakliga tyngdpunkten ligger därför snarare på att det skall vara begripligt än på att redovisa det allra, allra senaste från forskningsfronten.
Vi går först igenom några grundläggande definitioner för satslogiska bevissystem och antyder kopplingen till komplexitetsteori. Ett av målen i beviskomplexitet är att studera mer och mer avancerade bevissystem, relatera dessa system till varandra och bevisa undre gränser för dem. Vi tittar därför på två vanliga satslogiska bevissystem som används aktivt ute i verkligheten, resolution och skärande plan (Cutting Planes), och jämför dem.
Det visar sig att resolution kan beskrivas som ett tvåpersonersspel, där en lögnare påstår att en motsägelsefull formel kan satisfieras, medan en bevisare så enkelt som möjligt skall få lögnaren att snärja in sig i uppenbara motsägelser. Med hjälp av detta spel kan man visa att lögnaren kan ljuga så framgångsrikt om duvslagsprincipen (att n+1 duvor inte får plats i varsitt av n duvslag, även känd under namnet Dirichlets lådprincip) att det krävs exponentiella ansträngningar för bevisaren att avslöja honom. Eftersom skärande plan är minst lika starkt som resolution och dessutom har polynomiellt stora bevis för duvslagsprincipen visar detta att skärande plan är exponentiellt starkare än resolution.
Ett gitter är en diskret additiv delgrupp till R^n. Gitter har studerats ur en komplexitetsteoretisk vinkel sedan början av åttiotalet, och de senaste åren har ett flertal nya resultat kommit. Dessa resultat är av teoretiskt intresse, men är även användbara i kryptografiska sammanhang.
Som bakgrund kommer vi att gå igenom de grundläggande definitionerna för gitter och problemen att hittade en kortaste respektiva närmaste gittervektor (SVP resp CVP). Vi kommer också prata om kända resultat för dessa problem.
Därefter kommer vi att prata om hur man kan definiera en cykelstruktur för ett gitter och gå igenom resultat för hur cykelstrukturen påverkar svårigheten för SVP och CVP.
Deduktiv bevisföring räcker inte alltid till då man vill bevisa egenskaper hos till exempel mjukvarursystem. Testning eller simulering är inte heller tillräcklig om testrymden är någorlunda stor. En teknik som försöker råda bot på dessa problem är modellverifiering (model checking).
I mitt examensarbete undersöker jag en metod för att verifiera interaktionsegenskaper hos appletar. Metoden går ut på att extrahera alla metodanrop och bygga en anropsgraf som går att modellera som en kontextfri process. Denna kontextfria process kan sedan verifieras mot egenskaper beskrivna i en temporallogik kallad mykalkyl.
På seminariet kommer jag visa hur ett system av appletar kan modelleras som en kontextfri process, hur vissa typer av egenskaper kan formuleras i en delmängd till mykalkylen samt presentera en algoritm som kontrollerar om den uppställda modellen uppfyller de ställda kraven.
We introduce a stochastic calculus for program correctness that allows us to calculate the probability that a program S satisfies a Hoare triple {p}S{q}, contingent on the results of a finite set of black-box tests carried out on S. Correctness probabilities may be used as a measure of black-box test coverage.
We prove a 0-1 law for probabilistic program correctness which clarifies the scope and limits of testing from a logical viewpoint. Also we introduce techniques for the concrete calculation of correctness probabilities for computations over the ring of integers. These are based on random walk models of the finite dimensional distributions of programs and apply the reflection principle as a key tool for analysis.
I shall first explain how attempting to avoid information leaks when using Diffie-Hellman type cryptos leads to problems like the problem of being certain that quadratic residues exist in small intervals. I will then explain how, even though we are not sure that this can be done when computing modulo a large prime it can be done if one instead works with large finite fields of fixed characteristic.
Vi kommer att diskutera semidefinit programmering med tillämpningar inom approximation av NP-svåra optimeringsproblem. Exakt innehåll är inte spikat men vi kommer i alla fall gå igenom den numera klassiska approximationsalgoritmen för Max-Cut som hittades av Goemans och Williamson.
Primal-Dual metoden är en känd lösningsmetod för Linjär Programmering. Jag kommer att utgå från Goemans och Wiliamsons artikel om hur man kan använda Primal-Dual metoden för att hitta approximationsalgoritmer för kombinatoriska optimeringsproblem.
Klustring används inom språkteknologi för att dela in en mängd texter i kluster (delmängder) av texter. Målet är att texterna inom respektive kluster ska vara lika till innehåll.
Texterna representeras i den så kallade "vector space model" som även används i sökmotorer. Jag kommer att ge en introduktion till denna och någon klustringsalgoritm, samt utvärdering av klustringsresultat.
Biometri anses utgöra ett hot mot den personliga integriteten. Med nya tekniska lösningar kan detta förhållande ändras.
Efter en kort introduktion i biometri i allmänhet och fingeravtryck i synnerhet kommer jag att tala om några olika scenarier och möjliga lösningar, däribland match on card och en ny kryptografisk idé.
För betalningar som inte överstiger några kronor är de befintliga elektroniska betalningsmetoderna som kreditkort och betalkort olämpliga. Detta för att transaktionskostnaderna är för höga i förhållande till betalningens storlek. Probabilistiska system löser detta problem genom att bestämma probabilistiskt om betalning ska ske eller inte.
Syftet med detta seminarium är att gå igenom vilka krav som ställs på probabilistiska system, gå igenom exempel sådana system och berätta lite om för och nackdelarna med systemen.
Upp till webbsidan för doktorandseminarierna.