Home
Aktuelles
MitarbeiterInnen
Lehre
    SS08
    WS07/08
    Alle Semester
    Grundlegendes
    Diplomarbeiten
Forschung
    Kolloquium
    Gastvorträge
    Projekte
    Vorträge
    Publikationen
    Dissertationen
    Bücher
Aktivitäten
Opal
Impressum

Gastvorträge

Authentication in pervasive and social computation

Dusko Pavlovic
Kestrel Institute

Datum:

22.1.2008

Beschreibung:

In computer networks, information flows through a virtual space. In pervasive and social computation, information is also carried through physical space. This completely changes the security landscape.

In computer networks, the problem of authentication arises from the fact that all observations are local: a computer Alice can only observe her own actions, and therefore needs some solid cryptographic assumptions to prove to herself, say, that a computer Bob has indeed sent this message. However, if Alice and Bob are not computers on the Internet, but, say, PDAs in a cafe, then they can use their respective humans to observe each other's actions and in particular to directly authenticate some messages. This is something that computers on the Internet couldn't even dream about.

In this talk, I shall describe a framework for reasoning about authentication in the systems where some of the communication channels are deployed in a physical space.

Multi-Paradigmatic Model-Based Testing

	Wolfgang Grieskamp Microsoft Research
Datum:	29.9.2006
Beschreibung:	For half a decade model-based testing has been applied at Microsoft in the internal develop- ment process. Though a success story compared to other formal quality assurance approaches like verification, a break-through of the technology on a broader scale is not yet in sight. What are the obstacles? Some lessons can be learned from the past and will be discussed. An approach to MBT is described which is based on multi-paradigmatic modeling, which gives users the freedom to choose among programmatic and diagrammatic notations, as well as state-based and scenario- based styles, reflecting the different concerns in the process. The diverse model styles can be combined by model composition in order to achieve an integrated and collaborative model-based testing process. The approach is realized in the successor of Microsoft Research's MBT tool Spec Explorer, and has a formal foundation in the framework of action machines.

Program verification and testing at Microsoft Research

	Nikolai Tillmann Microsoft Research
Datum:	6.1.2006
Beschreibung:	This talk gives an overview of the ongoing research activities at Microsoft Research devoted to improving software development productivity using formal methods. In particular, I will introduce three methodologies which support the software development process in different stages. Each methodology is supported by tools: (1) Spec Explorer: system modeling and testing with model programs. (2) MUTT: better unit testing using symbolic execution to analyze existing implementations. (3) Spec# programming system: program verification by extending C# with pre/postconditions and invariants.

Tree Transducers - From Practice to Theory to Practice

	Dr.-Ing. Armin Kühnemann Institut für Theoretische Informatik Technische Universität Dresden
Datum:	10.2.2004
Beschreibung:	Ausgehend von vier praktischen Problemen, (i) der Definition einer formalen Semantik für imperative Programmiersprachen, (ii) der Spezifikation von XML-Transformationen, (iii) der Verbesserung der Effizienz funktionaler Programme, und (iv) der Verbesserung des automatischen Beweisbarkeit von Programmeigenschaften, motivieren wir die Theorie der Tree Transducer. Wir wählen zwei gegenläufige theoretische Resultate für Tree Transducer, die Komposition und die Dekomposition, aus und zeigen, daß sich diese auch in der Praxis anwenden lassen. Insbesondere demonstrieren wir, wie die Komposition und deren Weiterentwicklung Akkumulation die Effizienz von Programmen verbessern kann, und wie die Deakkumulation, eine Weiterentwicklung der Dekomposition, die automatische Verifizierbarkeit verbessern kann.

Drei Dimensionen der Array-Optimierung in SAC

	Dr. rer. nat. Clemens Grelck Institut für Softwaretechnik und Programmiersprachen der Universität zu Lübeck
Datum:	20.1.2004
Beschreibung:	SAC (Single Assignment C) ist eine rein-funktionale Arraysprache mit der Zielsetzung, Programmspezifikationen auf einem hohen Abstraktionsniveau mit einem hochperformanten Laufzeitverhalten zu verbinden. Der klassischen, von Maschinen-orientierten Progrmmiersprachen geprägten Sichtweise von Arrays als direkte Abbildungen in den Speicher mit lediglich rudimentären Indizierungsmöglichkeiten stellt SAC multidimensionale Arrays als abstrakte Datenstrukturen mit gewissen algebraischen Eigenschaften gegenüber. An die Stelle unübersichtlicher Schachtelungen von Schleifen zur Lösung eines individuellen Problems tritt das Prinzip der Komposition. Anwendungsprogramme entstehen durch stufenweise Komposition von einfachen und Problem-unspezifischen Array-Operationen zu immer komplexeren und immer Problem-spezifischeren Operationen. Dieses Prinzip führt nicht nur zu sehr knappen und abstrakten Programmspezifikationen, sondern erlaubt auch ein hohes Maß an Code-Wiederverwendung auf den verschiedenen Abstraktionsstufen. Leider läuft das Programmierkonzept der Komposition von Array-Operationen dem zweiten Ziel von SAC, dem effizienten Laufzeitverhalten kompilierter Programme, zuwider. Die direkte Übersetzung führt zwangsläufig zu ausführbarem Code, der zur Laufzeit eine sehr große Anzahl temporärer oder intermediärer Datenstrukturen erzeugt. Diese führen zu erheblichem organisatorischem Mehraufwand für Speicherverwaltung und Schleifenausführung, zu einer geringen Datenlokalität und insgesamt zu einem mehr als unbefriedigenden Laufzeitverhalten. Im Anschluss an eine kurze Einführung in die Prinzipien der Programmiersprache SAC identifizieren wir in dem Vortrag drei verschiedene Arten der Komposition von Array-Operationen und untersuchen jeweils die dadurch entstehenden Probleme und Herausforderungen für eine Übersetzung in effizienten Code. Für jede der drei Achsen des Problemfeldes wird eine konkrete Optimierungstechnik vorgestellt. Ihre aggregierte Wirkung wird an Hand einer Fallstudie untersucht.

Fehlersuche beim Debuggen nebenläufiger Programme

	Dr. Frank Huch Institut für Informatik und Praktische Mathematik Christian-Albrechts-Universität zu Kiel
Datum:	11.11.2003
Beschreibung:	Nebenläufige Systeme können neue, bei sequentiellen Systemen nicht auftretende Fehler enthalten, wie z.B. Deadlocks, Lifelocks oder die Nichteinhaltung von wechselseitigem Ausschluss. Im Gegensatz zu klassischen Fehlern sequentieller Programme, hängen diese Fehler vom Prozess-Scheduling ab und treten möglicherweise nur in bestimmten Systemläufen auf. Zum Finden von Fehlern werden in der Regel Debugger verwendet, welche den Programmablauf visualisieren und so ein besseres Verständnis der Fehlersituation ermöglichen sollen. Wir haben einen Debugger für Concurrent Haskell (eine nebenläufige Erweiterung der lazy- funktionalen Programmiersprache Haskell ) entwickelt. Dieser ermöglicht es, nebenläufige Haskell Programme auszuführen und manuell unterschiedliche Prozess-Scheduls auf Fehler zu überprüfen. Ein Nachteil dieses (auch bei den meisten anderen nebenläufigen Sprachen verwendeten) Ansatzes ist, dass sich ein System beispielsweise kurz vor einem Deadlock befinden kann, der Benutzer aber ein falsches Scheduling wählt und so den Programmfehler nicht findet. Als Lösung für dieses Problem soll der Debugger (alle) möglichen Schedules simulieren und im Fehlerfall den Benutzer in den Fehler leiten. Da nicht nur Deadlocks mögliche Fehler sind, soll die Linearzeit Logik (LTL) zur Spezifikation allgemeiner Fehlerzustände verwendet werden. Im Vortrag präsentieren wir die prototypische Implementierung des Debuggers, welche ohne eine Veränderung des Laufzeitsystems von Concurrent Haskell vorgenommen werden konnte.

Selektor-erzeugte Modelle verallgemeinerter logischer Programme

	Sibylle Schwarz Institut für Informatik der Universität Leipzig
Datum:	28.1.2003
Beschreibung:	Logische Programme sind gut geeignet zur Repräsentation von Fach- und Alltagswissen in Fakten- und Regelform. Im Vortrag wird eine Klasse modelltheoretischer Semantiken für verallgemeinerte logische Programme vorgestellt. Bei der Untersuchung einzelner Vertreter wird klar, daß sich viele prominente Semantiken (wie zum Beispiel die inflationäre Fixpunkt- und die stabile Semantik) als Spezialfälle davon darstellen lassen.

DNA-Computing - Rechnen mit Molekülen

	Dr.-Ing. Monika Sturm Technische Universität Dresden, Institut für Theoretische Informatik
Datum:	16.7.2002
Beschreibung:	In den letzten Jahren wurden in der Informatik verschiedene Ideen zur Entwicklung unkonventioneller Rechenmodelle verfolgt und realisiert. Alternativ zu klassischen Modellen basieren einige dieser Entwicklungen auf der Abstraktion biochemischer Prozesse. DNA-Computing stellt in diesem Zusammenhang eine spezielle Form für das Rechnen mit Molekülen dar. DNA dient dabei als Datenträger und die Rechenoperationen werden durch geeignete molekularbiologische und biochemische Prozesse realisiert. Ziel der Arbeiten an der TU Dresden ist die Entwicklung eines Modells für einen universellen DNA-Computer und dessen Implementierung im molekularbiologischen Labor. Algorithmen, die konstruiert werden, nutzen eine massive Datenparallelität, die es ermöglicht, mit DNA-Computern Rechengeschwindigkeiten zu erreichen, die einen Vergleich zu bekannter elektronischer Rechentechnik herausfordern. Der Vortrag thematisiert zunächst die Entwicklung des interdisziplinären Forschungsgebietes und stellt drei wichtige Aspekte in den Mittelpunkt. Die Vorstellung experimenteller Arbeiten soll zeigen, welche mathematischen Problemstellungen für DNA-Computing charakteristisch sind und welche Ergebnisse bisher erreicht wurden. Ein weiterer Aspekt beschäftigt sich mit der Fragestellung, wie ein theoretisches Modell aufgebaut sein könnte, welches DNA-Computing formal beschreibt, notwendige molekularbiologische Operationen umfaßt und laborpraktisch realisierbar ist. In einem letzten Aspekt soll betrachtet werden, wie ein funktional implementiertes Tool zur Konstruktion von DNA-Algorithmen und ein probabilistisches Simulationsmodell zur Vorbereitung von Experimenten eingesetzt werden.

Verification Diagrams: Graph+Logic+Automata

	Zohar Manna Stanford University
Datum:	9.4.2002
Beschreibung:	Verification Diagrams combine deductive ("theorem-proving") and algorithmic ("model-checking") verification to establish general temporal-logic properties of infinite-state reactive systems. The diagram serves as an abstraction of the system, while its underlying automaton represents the desired temporal behavior. We present two approaches: the use of w-automata (exponential) and alternating automata (linear).

Typisierung in Assemblersprachen mit Explizitem Forwarding

	Lennart Beringer University of Edinburgh, UK
Datum:	18.12.2001
Beschreibung:	Parallele Ausführung von Instruktionen und Result forwarding sind verbreitete Implementierungstechniken für moderne Prozessoren. In asynchronen Architekturen mit Operandenschlangen führt die gleichzeitige Benutzung beider Konzepte zu Komplikationen wie Deadlock oder Nichtdeterminismus. Um solche Interaktionen besser zu analysieren, führe ich eine Assemblersprache ALEF ein, in der beide Aspekte explizit sichtbar sind. Verschiedene Ausführungsmodelle können als unterschiedliche operationale Semantiken für diese Sprache aufgefaßt werden, und folglich mit programmiersprachlichen Methoden analysiert werden. Neben sequentieller Ausführung (instruction set architecture) werden wir parallele Ausführung betrachten, sowie Ausführungen, bei denen die Länge der Operandenschlangen begrenzt sind. Die für das jeweilige Ausführungsmodell auftretenden charakteristischen Fehlersituationen können in Analogie zum Vorgehen bei der Entwicklung von Programmiersprachen durch Typsysteme charakterisiert werden und so zur Compilezeit eliminiert werden. Typen beschreiben dabei Abstraktionen von Laufzeitkonfigurationen, basierend auf Notation aus Linearer Logik. Die Komponierbarkeit von Basisblöcken wird durch ein einfaches Unifikationsproblem dargestellt, ähnlich zu verwandten Problemen beim Typisieren von JVM code. Sollte die Zeit ausreichen, werde ich kurz Aspekte der Programmanalyse diskutieren, die bei der Übersetzung mit Zielsprache ALEF auftreten.