Student Talks at LMU - IfI (on BSc and MSc Level)
Week View - Agenda View - Plain HTML - Download or Import ICal Feed
- Fri, 06.03.
-
14:15–15:00
BDD-unterstützes SAT-Solving
BA Abschlussvortrag von Florian LeimgruberRaum: L109, Oettingenstr. 67 Organisator: TCSTalk details
Binary Decision Diagrams (BDDs) sind eine Datenstruktur zur Repräsentation Boolescher Funktionen, aus der sich viele Eigenschaften der Funktion leicht ablesen lassen. Um die Jahrtausendwende wurde die Effizienz von BDD basierten SAT-Solvern untersucht. Mit der Einführung des CDCL Algorithmus 1996 im Solver GRASP endeten diese Bemühungen größtenteils, da CDCL in der Praxis besser Performance zeigte. Mittlerweile basieren die meisten modernen SAT-Solver auf CDCL. Meine Bachelorarbeit griff BDD-basierte Ansätze wieder auf und untersuchte, wie hilfreich BDDs beim SAT-Solving sind. Es wurde dazu ein parallelen SAT-Solver entwickelt, die mithilfe von BDDs einen CDCL Solver unterstützen. Dabei werden BDD-Approximationsalgorithmen eingesetzt um die BDD-Größen zu limitieren. Die BDDs werden einerseits genutzt um lexikographische Suchraumeinschränkungen herzuleiten. Andererseits wurde ein Algorithmus entwickelt, der aus BDDs kleine Klauseln ableitet. Der Vortrag erläutert die Theorie hinter BDDs und CDCL, bevor erklärt wird, wie diese zu einem gemeinsam Solver kombiniert wurden. Zudem wird darauf eingegangen, worauf bei einer effizienten Implementierung geachtet werden muss. Zuletzt wird mit der experimentellen Evaluation belegt, dass die Suche nach kleinen Klauseln Vorteile bei ausgewählten kombinatorischen Problemen bringt.
-
14:15–15:00
Past talks
- Wed, 12.02.
-
12:30–13:00
SMT-based checking and synthesis of formal refinements
MA Antrittsvortrag von Tillmann GaidaRaum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
-
12:30–13:00
- Wed, 05.02.
-
12:30–12:40
Improve usability of summary tab for HTML tables of BenchExec
BA Antrittsvortrag von Dennis SimonRaum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
-
12:30–12:40
- Wed, 29.01.
-
12:30–13:15
Rely/Guarantee for Separation Logic in SecC
Masterprojekt Abschlusspraesentation von Bernhard PöttingerRaum: F003, Oettingenstr. 67 Organisator: SoSy-Lab -
13:30–14:00
Fault Localization with Error Invariants
BA Antrittsvortrag von Matthias KettlRaum: F003, Oettingenstr. 67 Organisator: SoSy-LabTalk details
There are many different ways to find out whether a program is buggy, for example testing or formal verification. Once we know that a program is buggy, i.e., that it shows some faulty behavior, a developer has to manually debug the program to find the cause of the problem and fix it - this is a difficult and long-taking process. The aim of the planned thesis is to help programmers with debugging by implementing Error Invariants and bug-finding with unsat cores, techniques for bug-finding based on boolean representations of the faulty program, to (1) automatically find potential causes for faulty behavior and (2) present the found causes. This talk is an overview talk for the planned thesis. -
14:00–14:25
Design and Implementation of a Cluster Based Approach for Software Verification
BA Presentation von Alexander RiedRaum: F003, Oettingenstr. 67 Organisator: SoSy-LabTalk details
Automatic software verification is a resource intensive process that often exceeds the capacity of a single machine. To tackle bigger programs, a way to add more computing power is needed. But hardware can not be upgraded indefinitely. One solution is to form a cluster out of several computers and use the combined computing power. To make the best use of the clustered resources, algorithms must be designed with increased latency and non-local data in mind. This thesis evaluates different ways of adding cluster support to an existing parallel verification algorithm that is part of the configurable software verification platform CPAchecker.
-
12:30–13:15
- Wed, 22.01.
-
12:30–13:00
Real-World Requirements for Software Analysis
BA Anstrittsvortrag von Amena AbdallaRaum: F003, Oettingenstr. 67 Organisator: SoSy-Lab -
13:15–13:45
Information Flow Testing für ein Modell eines PGP Servers
BA Antrittsvortrag von Lukas RiegerRaum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
-
12:30–13:00
- Tue, 14.01.
-
10:00–10:30
Octagon Analysis in CPAchecker (with ELINA)
BA Antrittsvortrag von Martin ZehendnerRaum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
-
10:00–10:30
- Thu, 09.01.
-
14:15–15:00
Unifikation von Multimengengleichungen von Variablen-zu-Variablen-Bindungen
BA Abschlussvortrag von Taro YoshiokaRaum: L109, Oettingenstr. 67 Organisator: TCSTalk details
Unfikationsprobleme zwischen Multimengen von Bindungen sind Gleichungen der Form {a_1 = b_1;...;a_n=b_n} = {x_1 = y_1;...;x_m=y_m}, wobei a_i, b_i, x_i, y_i sowohl feste Variablennamen oder instanziierbare Variablen für solche festen Namen sein dürfen. Solche Gleichungen können noch erweitert werden um Variablen, die ganze (Teil-)mengen solcher Multimengen repräsentieren. Im Rahmen einer Bachelorarbeit wurden Algorithmen zur Lösung solcher Unfikationsprobleme entwickelt und in der funktionalen Programmiersprache Haskell implementiert. Im Vortrag werden die Ergebnisse dieser Arbeit vorgestellt.
-
14:15–15:00