Student Talks at LMU - IfI (on BSc and MSc Level)
Week View - Agenda View - Plain HTML - Download or Import ICal Feed
- Wed, 04.11.
-
12:30–13:00
Real-World Requirements for Software Analysis
BA Abschlussvortrag von Amena AbdallaRaum: (online) Organisator: SoSy-Lab
-
12:30–13:00
Past talks
- Wed, 21.10.
- Wed, 30.09.
-
12:30–13:00
Fault Localization in Model Checking. Implementation and Evaluation of Fault-Localization Techniques with Distance Metrics
BA Abschlussvortrag von Angelos KafounisRaum: (online) Organisator: SoSy-Lab -
13:20–13:50
For The Win (FTW) Agent
Abschlussvortrag Praktikum zur Entwicklung eines groesseren Softwaresystems von Johannes TochtermannRaum: (online) Organisator: SoSy-Lab -
14:15–14:45
Integration und Evaluation von verketteten Entscheidungsdiagrammen in PJBDD und CPAchecker
BA Abschlussvortrag von Sebastian NiednerRaum: (online) Organisator: SoSy-Lab
-
12:30–13:00
- Wed, 16.09.
-
12:30–12:40
CWE-IDs for Software Analysis in CPAchecker and SV-COMP
BA Antrittsvortrag von Clara GoldmannRaum: (online) Organisator: SoSy-Lab -
12:50–13:20
Interval-based Optimization for SMT Solvers
BA Abschlussvortrag von Radu RusanuRaum: (online) Organisator: SoSy-LabTalk details
Symbolic execution is a program analysis technique, used to determine the inputs that execute a part of a program. The program is first converted to an execution tree, consisting of path conditions which may or may not be satisfiable. Variables are mapped to their symbolic input values (for boolean variables, the symbolic value is [0,1], for integer variables [−2^31, 2^31] and so forth) and then runs the program in order to find the reachable paths. Every path in the execution tree is parsed as a logical formula, which is defined as satisfiable if a model can be found which renders it as true, and tautological if every possible interpretation makes it true. Since most programs contain an abundance of numeral variables, a partial solver that narrows down the definition intervals of every variable and then performs the satisfiability-check is expected to speed up the solving, as the use of numbers instead of variables eliminates a considerable overhead. Since not every operation used by SMT-solvers is supported, a fallback to a complete solver is integrated if an unsupported operand is encountered. My implementation covers the theory of quantifier-free linear integer arithmetic (QF_LIA), however there is the possibility of expanding it to non-linear rational arithmetic and bit-vectors, which would model the semantics of imperative languages. The algorithm occurs in two stages - the learning stage, where the lower and upper bound of every variable are derived from the formulas passed as queries, and the decision stage where the variables are replaced with their respective intervals. The module is integrated into JavaSMT, an API developed by the Software and Computational Systems lab of the LMU München, which accesses common solvers like Z3 and SMTInterpol. -
13:35–14:20
Solver-based Analysis of Memory Safety using Separation Logic
MA Abschlussvortrag von Moritz BeckRaum: (online) Organisator: SoSy-Lab
-
12:30–12:40
- Wed, 02.09.
-
12:30–13:15
Test-based Fault Localization in the Context of Formal Verification: Implementation and Evaluation of the Tarantula Algorithm in CPAchecker
BA Abschlussvortrag von Schindar AliRaum: (online) Organisator: SoSy-Lab
-
12:30–13:15
- Wed, 22.07.
-
12:30–13:15
Fault Localization in CPAchecker with Error Invariants and UNSAT-Cores
BA Abschlussvortrag von Matthias KettlRaum: (online) Organisator: SoSy-Lab -
13:15–14:00
Energy Consumption Prediction of Verification Work
BA Abschlussvortrag von Petros IsaakidisRaum: (online) Organisator: SoSy-LabTalk details
Every aspect of our lives is nowadays being influenced by computer science, with its cornerstone being the compilation of computer programs that operate properly without malfunctions. For this purpose, the use of verification programs, such as the CPAchecker developed by the department of Software and Computational Systems at the LMU Munich, is essential. Nevertheless, these programs typically require considerable amounts of energy to conduct their verification tests. In order to minimize their power demands over time, monitoring of the required energy consumption is imperative. Intel’s Running Average Power Limit (RAPL) interface, which is usually implemented for this purpose, is software based and does not estimate the energy consumption of the whole computer system; thus, it is not suited for direct estimation of the whole system consumption. This thesis examines an alternative method of measuring the energy consumption of a system while running verification tests, using the EMH Metering ED300L energy meter. Our primary objective is to present the results of this approach and determine if there is a significant difference in energy estimation between the two methods. Furthermore, we aimed to propose an effective approach to predict the energy measurements of the energy meter based on Intel’s RAPL’s estimations while running verification tests on the CPAchecker software-verification platform. The overall goal of this thesis is to serve as an orientation to support the accurate energy usage measurement of a system.
-
12:30–13:15
- Wed, 15.07.
-
12:30–12:40
A Booge Frontend for Cuvee
BA Antrittsvortrag von Marius FunkRaum: (online) Organisator: SoSy-Lab -
12:45–13:30
A Web Frontend for Visualization of Computation Steps and their Results in CPAchecker
BA Abschlussvortrag von Sonja MünchowRaum: (online) Organisator: SoSy-Lab -
13:30–14:15
An IDE Plugin for CPAchecker
BA Abschlussvortrag von Adrian LeimeisterRaum: (online) Organisator: SoSy-Lab
-
12:30–12:40
- Wed, 01.07.
- Wed, 17.06.
- Wed, 10.06.
- Wed, 13.05.
-
12:30–13:15
Extending the Framework JavaSMT with the SMT Solver Yices2
BA Abschlussvortrag von Michael ObermeierRaum: (online) Organisator: SoSy-LabTalk details
JavaSMT, developed at the Software and Computational Systems Lab at LMU Munich, is a common API for SMT solvers. It offers access to a selection of solvers developed in Java as well as other programming languages. Support for those non-Java solvers is achieved through either existing or self-developed language bindings. While most solvers have a mostly identical core set of supported theories and features, they still differ by availability of additional theories and performance. As such adding more solvers to the framework will always be beneficial to the users. The Yices2 SMT solver, developed at SRI International’s Computer Science Laboratory was chosen as an addition because of its large feature set and extensive, well documented API. In this paper we will go over how the needed Java binding was developed and the integration with the JavaSMT API works. We will also cover the problems that were encountered while adapting the Yices2 API to JavaSMT’s and the solutions that were implemented. After covering the implementation, we will evaluate the performance of Yices2 against existing solvers in JavaSMT using the CPAchecker software verification framework and the SV-benchmarks set of verification tasks, which are also maintained at the SoSy-Lab. -
13:15–13:30
Code-Complexity Analysis on the Example of CPAchecker
BA Antrittsvortrag von Simon LundRaum: (online) Organisator: SoSy-Lab -
13:30–13:45
Support for Invariant Annotations from Correctness Witnesses in CPAchecker
BA Antrittsvortrag von Sven UmbrichtRaum: (online) Organisator: SoSy-Lab
-
12:30–13:15
- Wed, 06.05.
-
12:30–12:40
Fuzzing/Legion in CPAchecker
MA Antrittsvortrag von Christoph GirstenbreiRaum: (online) Organisator: SoSy-Lab
-
12:30–12:40
- Wed, 18.03.
-
12:30–13:15
Loop Contracts for Boogie and Dafny
Masterprojekt Abschlusspraesentation von Johannes BlauRaum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
-
12:30–13:15
- Wed, 11.03.
-
13:00–13:10
Fault Localization with Tarantula
BA Antrittsvortrag von Schindar AliRaum: 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 this thesis is to help programmers with debugging by implementing Tarantula, a technique for bug-finding based on test coverage, to (1) automatically find potential causes for faulty behavior and (2) present the found causes.
-
13:00–13:10
- 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
- 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