Lehrstuhlkolloquium Theoretische Informatik Universität Potsdam, Sommersemester 2010

In meiner Arbeit analysiere ich die Komplexität von SAT-Algorithmen, die auf dem DPLL-Kalkül basieren. Insbesondere suche ich nach unteren Schranken für diese Algorithmen. Die Basis für meine Arbeit ist der Ansatz von Alekhnovich et al. (2005), aus Expandern Formeln zu konstruieren, die für DPLL-Algorithmen schwer sind.

Im ersten Seminarvortrag war die Frage offen geblieben, ob Expander mit den erforderlichen Eigenschaften überhaupt existieren. Im aktuellen Vortrag zeige ich, dass diese Frage positiv beantwortet werden kann. Dazu gebe ich zunächst eine auf der probabilistischen Methode basierende Konstruktion an. Anschließend stelle ich eine auf dem Begriff der Kolmogorov-Komplexität basierende alternative Konstruktionsmethode dar.

Symmetrische Verschlüsselungsverfahren, wie zum Beispiel der Algorithmus AES, spielen heute eine große Rolle für eine sichere elektronische Kommunikation. Methoden aus der Kryptoanalyse können dazu genutzt werden, die Sicherheit symmetrischer Verfahren zu bestimmen. Beispielhaft seien hier genannt lineare und differentielle Kryptoanalyse, aber auch gruppentheoretische Betrachtungen.

Der Referent wird in seinem Vortrag darauf eingehen, wann diese Methoden an ihre Grenzen stoßen bzw. welche Fehler bei dem Design symmetrischer Verfahren gemacht werden können.

Dr. Marian Margraf ist Technischer Projektleiter "Elektronischer Personalausweis" im Referat Pass- und Ausweiswesen, Identifizierungssysteme, Bundesmelderegister im Bundesministerium des Innern. Im Rahmen dieser Tätigkeit koordiniert er die Forschung und Entwicklung der technischen Komponenten, die zukünftig im Umfeld des elektronischen Personalausweises eingesetzt werden.

The design of effective heuristic algorithms is a difficult process that traditionally requires considerable expertise and experience, often in combination with a substantial amount of trial and error.

In this talk, we outline a new approach for designing high-performance algorithms that is based on the use of automated procedures for exploring potentially very large spaces of candidate designs.We give an overview of several recent applications of this approach that allowed our group to achieve substantial improvements in the state of the art in solving SAT-encoded software verification, mixed integer programming and course timetabling problems.

In meiner Arbeit analysiere ich die Komplexität von SAT-Algorithmen, die auf dem DPLL-Kalkül basieren. Insbesondere suche ich nach unteren Schranken für diese Algorithmen. Alekhnovich et al. haben 2005 einen Ansatz für dieses Problem vorgestellt, der lineare Systeme über Expandern verwendet, um daraus für DPLL-Algorithmen schwere Formeln zu konstruieren.

In meinem Vortrag gehe ich zunächst auf den Begriff des Expanders ein, der sich in den letzten Jahren zu einem wichtigen Werkzeug der theoretischen Informatik entwickelt hat. Meine Betrachtung beschränkt sich auf diejenigen Eigenschaften von linearen Systemen über Expandern, auf denen die Konstruktion der unteren Schranken basiert. Danach gebe ich einen Überblick über die Beweisstrategie von Alekhnovich et al. und gehe auch auf einige Probleme ein, die bei der Analyse des Beweises sichtbar geworden sind.

Im Rahmen meiner Diplomarbeit habe ich mich mit Symmetrien in aussagenlogischen Formeln beschäftigt. Eine aussagenlogische Formel ist symmetrisch in einer Teilmenge ihrer Variablen, wenn man die Elemente dieser Teilmenge permutieren kann, ohne dass sich die Formel bezüglich bestimmter Kriterien verändert. Sind Symmetrien einer Formel bekannt, muss bei der Suche nach einer erfüllenden Belegung der Formel nur eine der zueinander symmetrischen Belegungen getestet werden, so dass die Suche durch Berücksichtigung der Symmetrien beschleunigt werden sollte.

Ich gebe in meinem Vortrag einen Überblick über verschiedene Verfahren zum Bestimmen oder Behandeln von Symmetrien. Um Herauszufinden, ob das Berücksichtigen von Symmetrien zu praktischen Verbesserungen beim Lösen von aussagenlogischen Formeln führt, habe ich empirische Untersuchungen mit einem ausgewählten Verfahren durchgeführt, deren Ergebnisse ich präsentiere. Abschließend stelle ich meine Weiterentwicklung des untersuchten Verfahrens vor, dass zu einer Verbesserung gegenüber dem ursprünglichen führt.

Das Nuprl-Beweisentwicklungssystem basiert auf der intuitionistischen Typentheorie. Durch konstruktives Schließen ermöglicht es die Extraktion von Programmen aus Beweisen. An vielen Stellen ist jedoch keine Konstruktion vonnöten : In Teilzielen, die lediglich einer ja/nein-Antwort bedürfen, erscheint deshalb eine Integration klassischer Logik sinnvoll. Um einerseits klassische Logik einsetzen zu können, andererseits jedoch sicherzustellen, dass sich dies im Extraktterm widerspiegelt, bietet sich als Grundlage der lambda-mu-nu-Kalkül von Pym und Ritter an. Allerdings arbeitet Pyms und Ritters Kalkül in Anlehnung an einen Sequenzenkalkül des natürlichen Schließens auf der rechten Seite der Sequenz und mit Multi-Konklusionen, während in Nuprl die Eliminationsregeln auf der linken Seite der Sequenz arbeiten und nur eine Formel (bzw. Typ) in der Konklusion zulässig ist. Eine direkte Simulation des lambda-mu-nu-Kalküls in Nuprl ist daher relativ umständlich, so dass eine entsprechende Umformulierung des Kalküls vorteilhafter erscheint.

Im Rahmen meiner Diplomarbeit beschäftige ich mich mit einer solchen Umformulierung des lambda-mu-nu-Kalküls in einen an die Refinement Logic angelehnten, analytischen Sequenzenkalkül, sowie dessen Eigenschaften und möglichen Erweiterungen. Dieser Vortrag dient im Wesentlichen zur Vorstellung des Themas.

Die Probabilistische Methode ist eine Technik, um die Existenz von bestimmten Objekten zu beweisen, indem man zeigt, dass das gesuchte Objekt in einem (geeigneten) Wahrscheinlichkeitsraum mit positiver Wahrscheinlichkeit p>0 auftritt. Ist p groß genug (z.B. p > 3/4), so lässt sich daraus ein probabilistischer Algorithmus konstruieren, der ein solches Objekt in erwarteter polynomieller Laufzeit findet.

Um die Existenz von Objekten zu beweisen, deren Auftrittswahrscheinlichkeit mit wachsender Problemgröße kleiner wird, eignet sich das Lovasz Local Lemma (LLL).

Wir stellen ein Schema vor, das auf der Grundlage des LLL einen probabilistischen Algorithmus mit erwarteter polynomieller Laufzeit zum Finden eines solchen Objektes erzeugt.

Das Car2Car Communication Consortium (C2C-CC) ist eine von europäischen Fahrzeugherstellern gegründete non-profit Organisation, die versucht, die Straßenverkehrssicherheit und -effizienz durch Fahrzeugkommunikation zu erhöhen.

Netzwerke von kooperierenden Fahrzeugen ermöglichen das Sammeln und Austauschen von sicherheitsrelevanten Informationen. Dazu gehören Informationen über Wetterverhältnisse, Straßenverhältnisse und Autounfälle. Die Kooperation der Fahrzeuge ermöglicht es, innerhalb von drei Minuten über einen Unfall informiert zu sein, der 50km entfernt geschehen ist. Die fortgeschrittene Kollisionswarnung sorgt zum Beispiel dafür, dass bei einer Vollbremsung die nachfolgenden Fahrzeuge gewarnt werden. Die Fahrzeuge geben die Warnung an ihre Fahrer weiter.

Unabdingbare Voraussetzung für den Einsatz der Fahrzeugkommunikation ist die Absicherung der Kommunikation. Dabei ist die Sicherstellung der Nachrichtenintegrität äußerst wichtig. Ein riskantes Fahrmanöver, das aufgrund von falschen Informationen durchgeführt wird, kann fatale Folgen haben. Daher ist ein Hauptsicherheitsziel des C2C-CC der Integritätsnachweis. Dieser liefert erstens den Nachweis, dass eine Nachricht beim angegebenen Urheber erzeugt wurde und zweitens, dass sie auf ihrem Weg durch das Netzwerk nicht verändert wurde.

In dieser Diplomarbeit wird ein Mechanismus entwickelt, der das Sicherheitsziel Integritätsnachweis für C2C Anwendungen gemäß den Anforderungen des C2C-CC umsetzt. Drei wesentliche Anforderungen sind eine schnelle Ausführung, eine hohe Skalierbarkeit und ein Entwurf basierend auf bestehenden Konzepten, Methoden und Algorithmen. Es werden traditionelle Public-Key Kryptographie, identitätsbasierte Kryptographie und zertifikatslose Kryptographie betrachtet.

Es stellt sich heraus, dass die traditionelle Public-Key Kryptographie am wenigsten geeignet ist. Beim Vergleich der identitätsbasierten Kryptographie und der zertifikatslosen Public-Key Kryptographie entsteht eine Trade-Off Situation zwischen Effizienz und Sicherheit.

Die Arbeit hat das Ziel, einen Grundstein für die Entwicklung eines zeitgemäßen Editors für FDL zu legen. Zu diesem Zweck wurden verschiedene Komponenten entwickelt, die im Vortrag kurz vorgestellt werden sollen: das Gui Framework als solches, ein Modul zum Darstellen von Termen mit Displayformen und eine generische Datenstruktur zum Editieren von Termen.

Es werden die Ziele und das Arbeitsprogramm dargestellt, die in einem eingereichten DFG-Antrag beschrieben wurden. Zuvor wird kurz in die Syntax und Semantik von modaler Aussagen- und Prädikatenlogik eingeführt.

zum Projekt (Jens Otten):

Dabei geht es um die Modellierung von Sicherheitsanforderungen in verteilten, heterogenen Systemen. Ziel der Kooperation ist der Einsatz von formalen Methoden und eines Theorem-Beweisers um die Konsistenz dieser Anforderungen sicherzustellen.

Als wesentlichen Baustein für die Synthese von probabilistischen Algorithmen benötigen wir eine Formalisierung der wahrscheinlichkeitstheoretischen Grundlagen.

Um zufällige "Funktionen" zu modellieren , sollen Bernoulli-(1/2)-Folgen verwendet werden. Im Vortrag werde ich zeigen, wie die dazugehörige Ereignisalgebra und das Wahrscheinlichkeitsmaß darauf aussieht, welche Probleme bei der Formalisierung auftreten und wie diese eventuell zu lösen sind.

Um probabilistische Programme automatisch zu synthetisieren brauchen wir eine geeignete formale Darstellung probabilistischer Funktionen. Eine solche Darstellung bietet die in dem Artikel "Probabilistic Lambda-Calculus and Quantitative Program Analysis" von Di Pierro, Hankin und Wiclicki vorgestellte Erweiterung des klassischen (ungetypten) Lambda-Kalküls.

Im Vortrag sollen der Kalkül und die beiden Formen der operativen Semantik dargestellt werden.

Mitte der 90er Jahre wurden von Beame, Impagliazzo, Pitassi und anderen verschiedene Übersetzungen des Erfüllbarkeitsproblems für aussagenlogische Formeln in Standardprobleme der kommutativen Algebra wie ideal membership vorgeschlagen. Der Gröbnerbasis-Algorithmus kann dann zur Beweissuche verwendet werden.

Ziel des Vortrags ist es, den Gröbnerbasis-Algorithmus, die Übersetzung selbst, und einige (ebenfalls Mitte/Ende der 90er) damit erzielte Resultate zur Beweiskomplexität vorzustellen.

Mittelfristiges Ziel ist die (bisher offensichtlich kaum betriebene) Untersuchung der Effizienz der Beweissuche mittels solcher Systeme.

Der Entwurf klassischer dreischichtiger Datenbankapplikationen erfordert in der Regel, die zugrundeliegende Geschäftslogik zu weiten Teilen in allen drei Schichten separat zu implementieren. Neben der mehrfachen Implementierungsarbeit birgt ein solches Vorgehen vor allem die Gefahr von Inkonsistenzen zwischen den einzelnen Schichten, die um so größer wird, je mehr Weiterentwicklungszyklen die Applikation erfährt. Wünschenswert wäre daher eine Entwicklungsumgebung für die abstrakte Spezifikation der Geschäftslogik, aus der heraus die Implementierung aller drei Schichten automatisch generiert werden kann.

Die von Microsoft in VisualStudio 2005 integrierte Möglichkeit, eigene sogenannte "Domain Specific Languages" in die Entwicklungs- umgebung zu integrieren, bietet einen ausgesprochen interessanten Rahmen, um einen derartigen Designer für Geschäftslogik der allgemeinen Entwicklergemeinde nahe zu bringen. Für die eigentliche Formalisierung der Geschäftslogik sowie die Herleitung passender Implementierungen aller drei Schichten aus einer solchen Formalisierung böte sich indessen ein spezialisierter Ansatz auf Basis der Konstruktiven Typentheorie und den zugehörigen Deduktionsverfahren an.

Auf diese Weise könnte es zum einen gelingen, der Programmsynthese-Gemeinde den Durchbruch zum Entwickler-Alltag zur ermöglichen. Andererseits würde aber auch die praktische Entwicklergemeinde einen enormen Gewinn aus den wesentlich verkürzten Entwicklungs- und Debuggingzyklen beziehen, die sich potentiell aus der Nutzung eines derartigen abstrakten Systems ergeben können. Der Vortrag möchte daher eine Industriekooperation zur Entwicklung eines entsprechenden Gesamtsystems anregen.

Wie konstruktiv ist konstruktiv? Wann lassen sich im Zuge einer intuitionistischen Beweisführung konstruktive Schlussweisen korrektheitserhaltend durch weniger aufwändige nicht-konstruktive Schlussweisen ersetzen? Dieser Vortrag stellt das Prinzip der "konstruktiven Adäquatheit" in den Mittelpunkt eines Ansatzes zur Beantwortung dieser Fragen. Aufbauend auf einer modelltheoretischen Analyse des konstruktiven Gehalts konstruktiver Inferenzregeln wird eine Beweistheorie entwickelt, die jene konstruktive Schlussweisen unter bestimmten Umständen korrektheitserhaltend vermeidet. Die dem zugrunde liegenden Überlegungen führen darüber hinaus auch dazu, dass intuitionistische Duplikationen unter bestimmten Voraussetzungen vermieden werden können.

Insgesamt entsteht damit eine Beweistheorie, deren sämtliche Schlussweisen invertierbar sind und bei der gleichzeitig jede Herleitung einer aussagenlogischen Formel garantiert nach endlich vielen Schritten terminiert. Schließlich wird gezeigt werden, wie sich diese Theorie in effizienzorientierte Beweisverfahren integrieren lässt.

ILTP-Library:

Gleichheitsbehandlung:

JProver-SAT/QBF-Solver-Kombination:

The main aim of my thesis is to provide a set of concepts and tools for the automation of the real-time embedded software testing according to the newest technologies, methodologies and requirements.

Summing up, the idea of this work is to automate testing development parallel to system development. The innovation in relation to the standard software engineering is the analysis of testing processes regarding the input signal types (continuous, discrete) and real-time constraints. One has to go away from structure oriented towards function (behaviour) oriented approaches. However, model-based testing and Model Driven Architecture (MDA) ideas are still valid.

My speech is divided according to the following outline. As introduction - problems and aims of the work are presented. After that, the main definitions of embedded, hybrid and real-time reactive systems are provided. Testing and its role in the V-Model must be also depicted. State of the art (i.e. existing methodologies and tools for automotive industry) is shortly mentioned. Further on, the major focus is put on the core of the thesis, which means requirements-driven and model-based testing of real-time embedded systems. These processes are described, methodology of the problems solution is given and their integration by help of MDA artefacts is depicted. Finally, time schedule, summary and outlook are provided. Last, but not least my newest research results (not published yet) are mentioned.

The Supervisor of the thesis is: Prof. Dr. -Ing. Ina Schieferdecker from Technical University Berlin (Entwurf und Testen von Telekommunikationssystemen)