Vorträge
Informatik-Kolloquium Prof. Schneider
Es spricht Herr Prof. Dr. Stefan-Alexander Schneider, Lehrgebiet Grundlagen der Fahrerassistenzsysteme, Hochschule Kempten, spricht zum Thema:
"IT as Enabler for Advanced Driver Assistance Systems"
am Mittwoch, 24.02.2016
um 9:00 Uhr
im Hauptgebäude 0.18
Abstract
Wir laden alle Interessenten recht herzlich ein.
Informatik-Kolloquium: Prof. Dr. Ute Schmid
Es spricht Frau Prof. Dr. Ute Schmid (Universität Bamberg)
zum Thema "Lernen auf der Wissensebene".
Das Fachgebiet Programmiersprachen und Compilerbau lädt alle Interessenten
am Freitag, 17.05.2013
um 9:30 Uhr
im Hauptgebäude, Raum 0.17
recht herzlich ein. Einladung mit Abstract
Gemeinsames Kolloqium
Das Fachgebiet Energiewirtschaft und das Fachgebiet Programmiersprachen und Compilerbau freuen sich,
Herrn PD Dr. Cyrill Stachniss von der Universität Freiburg
zu einem Vortrag begrüßen zu können.
Titel:
Probabilistische Methoden für die Roboternavigation –
von grundlegenden Problemen zu realen Systemen
Die Veranstaltung findet am Donnerstag, den 14.02.201
ab 16.00 Uhr s.t. im LG 3A – Raum 324 statt.
12. GI/ITG KuVS Fachgespräch "Drahtlose Sensornetze"
Am 12. und 13. September 2013 findet das 12. GI/ITG KuVS Fachgespräch "Sensornetze" der von GI und ITG (VDE) gemeinsam getragenen Fachgruppe Kommunikation und Verteilte Systeme (KuVS) an der Brandenburgischen Technischen Universität statt. Es wird organisiert vom Lehrstuhl Verteilte Systeme / Betriebssysteme.
Weitere Informationen finden Sie auf der Webseite des 12. GI/ITG KuVS Fachgespräches "Sensornetze".
Informatik-Kolloquium: Thomas Hinze
Dr.-Ing. Thomas Hinze, BTU Cottbus, Institut für Informatik, spricht zum Thema:
"Rechnen mit Molekülen: Neue Impulse und Herausforderungen einer jungen biologisch inspirierten Informatikdisziplin"
Alle Interessenten sind herzlich eingeladen!
Termin: Montag, 09.07.2012 um 10:00 Uh
Ort: Hauptgebäude der BTU, Raum 2.4
Weitere Informationen: Einladung/Abstract
Informatik-Kolloquium
Dipl.-Inf. Thomas König spricht zum Thema:
"Komplexität von booleschen CSPs mit eingeschränkten Constraint-Sprachen"
am Montag, 02.07.2012 um 9:00 Uhr im Hauptgebäude Raum 2.13
Informatik-Kolloquium
Frau Anna Prenzel (Hochschule Zittau/Görlitz)
hält einen Vortrag zum Thema:
„Gestaltung der Mensch-Computer-Interaktion zur
Entscheidungsunterstützung bei Dispositionsaufgaben“
am Dienstag, den 13.03.2012, 10:30 Uhr
im Hauptgebäude, Raum 2.13
Informatik-Kolloquium
Herr Alexander Bau
Hochschule für Technik, Wirtschaft und Kultur Leipzig
hält einen Vortrag zum Thema:
"Constraint Programmierung via Haskell Programmierung"
Montag, 16.01.2012, 10:30 Uhr
Hauptgebäude, Raum 2.13
Vortrag und Hands-On im Rahmen von Haskell in Leipzig 5
Dependent Types mit Agda
Vortragender: Wolfgang Jeltsch
am 04.06.2010, 15:45 Uhr (Vortrag) und 17.00 Uhr (Hands-On) auf dem Leipziger Mediencampus
Mit abhängigen Typen (dependent types) können nicht nur Typen, sondern auch Werte als Parameter von Typen fungieren. Dadurch kann man z.B. die Längen von Listen in deren Typen angeben. Damit wird es möglich, fehlerhafte Indizierungen zur Compilierzeit statt zur Laufzeit zu erkennen.
Die Möglichkeiten reichen aber noch viel weiter. Eine Programmiersprache mit abhängigen Typen ist nämlich automatisch eine Beweissprache für eine Prädikatenlogik. Daher kann man nahezu beliebige Spezifikationen als Typen darstellen und deren Einhaltung vom Typprüfer sicher stellen lassen.
In dem Vortrag und dem anschließenden praktischen Teil werden folgende Themen behandelt:
- Grundlagen zu Dependent Types
- Grundlagen zu induktiven Familien (GADTs)
- die Grundidee des Curry-Howard-Isomorphismus
- ein kleiner Beweis in Agda
Folgende Beispiele werden gezeigt:
- statische Bereichsprüfung für Listenindizes
- take mit Bereichsprüfung für die Resultatlänge
Vortrag im Rahmen des Informatik-Kolloquiums
Lazy Evaluation in der computergestützten Komposition
Vortragender: Diplom Komponist Kilian Sprotte
am Mittwoch, 10.03.2010, 13:30 Uhr, Hauptgebäude, Raum 2.44
Zusammenfassung:
Grafische Programmiersprachen, die in der Form von Blockdiagrammen die Modellierung musikalischer Prozesse erlauben, finden bereits häufig Verwendung. Sie lassen sich grob in zwei Gruppen einteilen. Auf der einen Seite ist ein System wie "Pure Data" überwiegend zur Klangsynthese geeignet, während auf der anderen Seite eine Kompositionsumgebung wie "OpenMusic" oder "PWGL" die Arbeit an übergeordneten Strukturen, angefangen bei Notenereignissen bis zur globalen Form erlaubt.
Es wird ein Prototyp einer solchen grafischen Programmiersprache vorgestellt, die in Lisp eingebettet ist, aber auf einem Lazy Dialekt aufsetzt und prinzipiell beide Anwendungsgebiete vereint. Dazu werden Beispiele gezeigt und auch verschiedene Datenstrukturen zur Musikrepräsentation vorgestellt.
Short Bio:
Kilian Sprotte studierte Komposition bei Prof. Younghi Pagh-Paan und Elektronische Musik bei Günter Steinke an der HfK Bremen. Zu seinen Werken gehören überwiegend instrumentale Kompositionen, aber auch Klanginstallationen und Arbeiten mit Video.
Er interessierte sich zunehmend für die computergestützte Komposition, wurde am IRCAM, Paris für ein Jahr in die Music Representation Group als Gastforscher eingeladen und hat seitdem in verschiedenen - überwiegend lisp-basierten - Softwareprojekten mitgewirkt, so auch seit 2007 an der Kompositions-umgebung PWGL.
Vortrag im Rahmen des Informatik-Kolloquiums
Model Checking als Ansatz zur Verifikation digitaler und eingebetteter Systeme
Vortragender: Dipl.-Ing. Thilo Vörtler
am Donnerstag, 04.03.2010, 11:00 Uhr, Hauptgebäude, Raum 2.13
Zusammenfassung:
Eingebettete Systeme bestehen meist aus einer Kombination von Hardware, Software und Sensoren. Sie werden in einer Vielzahl von Anwendungsbereichen und Geräten verwendet, z.B. in der Automobilbranche oder der Medizintechnik.
Model Checking ist eine Verifikationstechnik die es erlaubt, die funktionale Korrektheit nicht nur durch Simulation zu überprüfen, sondern die Korrektheit von Systemeigenschaften zu beweisen. Beim Entwurf digitaler Schaltungen wird Model Checking, ergänzend zur Simulation, als Methode zur Überprüfung von kritischen Eigenschaften bereits verwendet. Auch für die Verifikation von Software eines eingebetteten Systems lässt sich Model Checking verwenden, wobei insbesondere die Verifikation im Zusammenspiel mit Hardware eine Herausforderung darstellt.Im Vortrag wird Model Checking als Methode zur Verifikation von digitalen Systemen vorgestellt. Es werden praktische Probleme erläutert, welche bei der Verifikation von Digitalentwürfen auftreten. Außerdem wird Software Model Checking vorgestellt, welche es ermöglicht Software für eingebettete Systeme zu überprüfen.
Vortrag im Rahmen des Informatik-Kolloquiums
Beispielgetriebene Schemainduktion beim induktiven Programmieren
Vortragender: Dipl.-Wirtsch.Inf. (E.M.B.Sc.) Martin Hofmann
Otto-Friedrich-Universität Bamberg
am Mittwoch, 27.1.2010, 14:00 Uhr, Hauptgebäude, Raum 2.13
Zusammenfassung:
Induktives Programmieren (IP) beschäftigt sich mit dem Erzeugen (rekursiver) Programme aus unvollständigen Spezifikationen, in der Regel Eingabe- / Ausgabebeispielen. Alle bekannten IP Algorithmen können als Suche im Raum aller Kandidatenprogramme aufgefasst werden, mit folglich exponentiellem Aufwand.
Um den Suchaufwand zu beschränken und den Suchraum zu reduzieren, können Programmschemata verwendet werden. Allerdings muss entweder ein (oft sehr gut) informierter Benutzer ein Schema a priori vorgeben, oder verschiedene Schemata werden einfach wahllos ausprobiert. In der anschließenden Synthese werden nun alle Daten in Hinblick auf dieses eine gegebene Schema interpretiert welches folglich nun gewissermaßen ausschließlich über Erfolg oder Misserfolg entscheidet.
Anstelle nun die gegebenen Daten „in ein Schema zu pressen“, stellen wir einen Ansatz vor, der es erlaubt anhand der Daten ein Schema zu induzieren. Wir nutzen dazu universelle Eigenschaften von Funktionen höherer Ordnung, die sich in den Eingabe- /Ausgabedaten finden lassen. Diese Technik erlaubt es uns, Catamorphismen auf allgemeinen algebraischen Datenstrukturen in unserem IP System Igor2 einzuführen.
Vortrag im Rahmen des Lehrstuhl-Kolloquiums
Generische Record-Kombinatoren mit statischer Typprüfung
Vortragender: Dipl.-Inf. Wolfgang Jeltsch
am 13.01.2010, 13:45 Uhr, Hauptgebäude, Raum 2.13
Zusammenfassung:
Records, d.h. Kollektionen von benannten Feldern, sind ein wesentlicher Bestandteil vieler Programmiersprachen. Neben dem Zugriff auf einzelne Felder spielen dabei Operationen auf gesamten Records, sogenannte Kombinatoren, eine wichtige Rolle. Record-Kombinatoren müssen oftmals generisch sein, also mit Records verschiedener Struktur arbeiten. Generische Record-Kombinatoren können im Allgemeinen nur in dynamisch typisierten Sprachen definiert werden.
In dem Vortrag wird ein Record-System für die Programmiersprache Haskell vorgestellt, welches die Definition statisch typisierter generischer Record-Kombinatoren ermöglicht. Dieses System ist als Bibliothek implementiert, kommt also ohne Änderungen an der Programmiersprache aus. Ermöglicht wird das vor allem durch die Nutzung fortgeschrittener Typsystemkonzepte.
Vortrag im Rahmen des Informatik-Kolloquiums
Programmierung und Verifikation reaktiver Systeme mittels funktionaler Programmierung
Vortragender: Dipl.-Inf. Wolfgang Jeltsch
am 18.11.2009, 13:45 Uhr, Hauptgebäude, Raum 2.13
Zusammenfassung:
Funktionale Reaktive Programmierung (FRP) ist ein Paradigma, mit dessen Hilfe reaktive und interaktive Systeme deklarativ programmiert werden können. Der Programmierer beschreibt zeitliches Verhalten von Systemkomponenten mittels kontinuierlicher und diskreter Signale, welche zeitveränderliche Werte bzw. Ereignisfolgen darstellen. Dabei können durch Signal-Operatoren aus einfachen Signalen komplexe Signale aufgebaut werden.
Der Vortrag gibt zunächst eine Einführung in die Grundkonzepte von FRP. Anschließend behandelt er typische Probleme der Implementierung von FRP-Bibliotheken und zeigt Lösungen auf. Schließlich geht er auf die enge Beziehung zwischen FRP und temporaler Logik ein und deutet an, wie diese für die Verifikation reaktiver Systeme nutzbar gemacht werden kann.