Student Talks at LMU - IfI (on BSc and MSc Level)
Week View - Agenda View - Plain HTML - Download or Import ICal Feed
Past talks
- Wed, 10.11.
-
14:30–14:50
New Approaches and Visualization for Verification Coverage
MA Antrittsvortrag von Maximilian HailerRaum: (online) Organisator: SoSy-Lab -
14:50–15:25
SV-COMP Benchmarks for Weak Memory Models
BA Abschlussvortrag von Korab ZoguRaum: (online) Organisator: SoSy-LabTalk details
The International Competition on Software Verification allows a rigorous comparison of state-of-the-art verification tools through a unified benchmark set. The current benchmark set does not include a memory model aware category for verification tools which are sensitive to the subtle differences in program behaviour that results from different processor architectures using different memory models or compiler optimizations that produce binaries with relaxed memory guarantees. A large benchmark set of benchmarks, categorized by different architectures, already exists in the DAT3M suite. The format of the existing benchmark files does not fit into the standard format set by the SV-COMP rules, especially with regards to the program language of the given benchmark tasks. The goal of this thesis is to transform the existing benchmarks, which are written in an assembly-like language, into valid C programs with a valid assertion. This way, a set of valid verification task can be added to SV-COMP, which would be enriched by a new, memory model aware benchmarking category. The details, encountered problems and final results are shown and discussed. Furthermore, limitations of the practical implementation and future work is looked at and suggestions for the continuation of this work are made. In the end, two of the four cate- gories (AARCH64, PPC, X86, C) are successfully transformed with a success rate of 100%. The other two categories are still not fully implemented, with moderate success rates in the transformations resulting in a conversion rate of 52% in the C (linux-kernel) category and 24% in the AARCH64 category. Possible solution approaches and the severity of the partially successfull categories are also discussed. The general process of converting the benchmark has seen substantial success and the final process for closure of the other categories is time intensive but straightforward. -
15:35–16:10
Genetic Programming in Software Verification
BA Abschlussvortrag von Ludwig GlückstadtRaum: (online) Organisator: SoSy-LabTalk details
Genetic programming is a well-known and effective algorithm for optimization problems. However, possibly due to long round trip times between generations, its use is absent in software verification. We do think that it is possible to use genetic programming effectively in this field. For this we want to build a framework that can easily be adjusted and used by researchers. Possible applications for this framework are automatically generating tasks to benchmark verification software, finding tasks that are hard to verify with one method but easy with others, and possibly even fault localization. The framework uses BenchExec to execute verification software at every step and use the results for the next steps of the algorithm. We found that our framework was effective at producing hard to verify tasks, but not usable in fault localization. However, the round trip time was significant and added to the overall wall time of the algorithm execution. We still think that our framework can fill a niche in software verification by automatically generating verification tasks that fulfill specific parameters.
-
14:30–14:50
- Wed, 03.11.
-
15:00–15:45
Effcient Software Model Checking with Block-Abstraction Memoization
Disputation von Karlheinz FriedbergerRaum: Hauptgebäude A120 and online via Zoom Organisator: SoSy-LabTalk details
In the last decades, the research community has made several steps towards better usage, adaptation, and understanding of formal techniques. However, due to their high demand of resources in both manpower as well as computational effort, formal methods are still not as used in the standard software development process as plain testing, but almost exclusively in critical applications, where a failure can get life-threatening or disproportionately expensive. Our studies on scalable and modular approaches show the potential of block-abstraction memoization, which is a verification technique based on a divide-and-conquer strategy that leverages the internal structure of a program. Using an abstract domain like predicate abstraction, value analysis, or combinations thereof, we evaluate the approach on a large and established benchmark set to provide evidence for its competitive performance against other state-of-the-art approaches and also to show its potential in (1) using CPUs with multiple cores to their full potential and (2) the application to recursive programs. Additionally (3) we give insights into different refinement strategies for this verification technique.
-
15:00–15:45
- Wed, 20.10.
-
14:30–15:00
Iterated Prisoner's Dilemma with Players Learning to Provide Unpaid and Paid Incentives to Others
BA Abschlussvortrag von Xiyue SunRaum: (online) Organisator: SoSy-Lab -
15:00–15:30
Linear Interpolation of Multiple Objectives
BA Abschlussvortrag von Mario QuittRaum: (online) Organisator: SoSy-Lab -
15:30–16:00
Leveraging Curricula to Explore Pareto Fronts in Multi-Objective Reinforcement Learning
BA Abschlussvortrag von Philip AdamczykRaum: (online) Organisator: SoSy-Lab
-
14:30–15:00
- Wed, 13.10.
-
14:30–15:05
CWE-Ids for Software Analysis in CPAchecker
BA Abschlussvortrag von Clara Sofie GoldmannRaum: (online) Organisator: SoSy-LabTalk details
In the development of software, there can be errors that can lead to unintended results during execution. To prevent this, each software should be tested and carry out formal verification. In this work we will deal exclusively with formal verification and use the formal verification tool CPAchecker. Formal verification is used to eliminate unwanted behavior and errors in a software and to prove the correctness of the software against a specification. There are several approaches to formal verification, two being are for example Data-Flow Analysis or Model Checking. The framework CPAchecker combines both approaches, model checking and data flow analysis, and thus brings out the best in both approaches. CPAchecker statically analyzes the program, constructs an abstract model, and finally looks to see if the specification is met based on the entire set of states. The specification describes properties of the program, such as safety or liveness, that must be satisfied in order for the program to be correctly checked with respect to the specification. In this work we look at a range of well-known properties, e.g. available as example programs in the Juliet benchmark suite, and analyse them with CPAchecker. The main goal is to create an overview of CWE-Ids which CPAchecker can recognize. CWE stands for ’Common Weakness Enumeration’, where the CWE-Ids each describe different vulnerabilities. During the evaluation of these CWE-Ids we came across with some difficulties CPAchecker has to handle.
-
14:30–15:05
- Wed, 22.09.
-
14:30–15:05
Implementation and Evaluation of tagged BDDs in PJBDD
BA Abschlussvortrag von Simon RathsRaum: (online) Organisator: SoSy-Lab -
15:15–15:30
Adjustable Block Analysis: Actor-based block summaries for scaling formal verification
MA Antrittsvortrag von Matthias KettlRaum: (online) Organisator: SoSy-Lab
-
14:30–15:05
- Wed, 28.07.
-
14:30–14:40
A CPA for String Analysis for Java Programs in CPAchecker
BA Antrittsvortrag von Simon AntonischkiRaum: (online) Organisator: SoSy-Lab -
14:50–15:00
Use cgroups v2 for BenchExec to improve container isolation
BA Antrittsvortrag von Robin GlosterRaum: (online) Organisator: SoSy-Lab -
15:10–15:35
Implementation and Evaluation of a Simple Taint Analysis for CPAchecker
BA Abschlussvortrag von Robin GlosterRaum: (online) Organisator: SoSy-Lab
-
14:30–14:40
- Fri, 11.06.
-
14:15–15:00
Antrittsvortrag Bachelorarbeit: Codierung und Decodierung von Faltungscodes durch deterministische Transduktoren
von Johannes SchlüßlhuberRaum: L109, Oettingenstr. 67 Organisator: TCSTalk details
Faltungscodes sind eine Codeklasse der Kanalcodierung und unterscheiden sich durch ihre dynamische Eingabelänge von den Blockcodes. Durch zusätzliche Redundanz bieten sie eine Vorwärtsfehlerkorrektur. Faltungscodierer werden meistens durch Schieberegister beschrieben, können aber auch durch äquivalente Zustandsautomaten genauer gesagt deterministische Transduktoren dargestellt werden. Zum Decodieren wird standardmäßig der Viterbi-Algorithmus verwendet. Transduktoren sind endliche Automaten, welche zusätzlich noch eine Ausgabefunktion besitzen. In dieser Arbeit werden nun Faltungscodes durch deterministische Transduktoren codiert und auch decodiert. Das Ziel ist das Finden von geeigneten Decodierern und passenden Codierer-Decodierer Paaren in Form von deterministischen Transduktoren. Hierfür werden als Methoden die Zufallssuche, ein evolutionärer Algorithmus und SAT-Solving verwendet. -
14:15–15:00
Antrittsvortrag Bachelorarbeit: Automatenlernen mit Ant Colony Optimization Algorithmen
von Leonard GanzRaum: L109, Oettingenstr. 67 Organisator: TCSTalk details
Die Konzepte der von der Natur inspirierten Ant Colony Optimization Algorithmen sollen auf das Automatenlernen übertragen werden. Mit einer Menge an Wörtern werden in mehreren Iterationen Automaten mit probabilistischen Übergängen konstruiert. Über positives und negatives Feedback sollen sich dabei einzelne Übergänge herauskristallisieren, mit denen später ein deterministischer Automat abgeleitet werden kann. Die vielen Stellschrauben des Lernalgorithmus gilt es im Laufe des Projekts zu optimieren. Neben der Kernfunktionalität stehen zahlreiche weitere Möglichkeiten für Erweiterungen, Anpassungen und Experimente bereit.
-
14:15–15:00
- Fri, 28.05.
-
14:15–15:00
Checked Exceptions for Haskell
von Philipp ZanderRaum: L109, Oettingenstr. 67 Organisator: TCSTalk details
Checked exceptions make the exceptions a function may raise to its caller part of its statically checked type. One benefit of that is that there will not be any unanticipated exceptions at run time. I propose an approach to making checked exceptions available to Haskell programmers piggybacking on Haskell's powerful type system. And implement it as a Haskell library. I explain why this approach is currently unacceptably inefficient. I describe a small modification to the Glasgow Haskell Compiler that would make the proposed approach work very well and which is reasonable and useful on its own. I list a variety of alternative approaches to providing checked exceptions through a Haskell library. I define a set of significant comparison criteria, which I evaluate all approaches by. I show that the proposed approach is superior to all alternatives. This thesis has got the following two main goals. The primary goal is to convince the reader of the appeal of the proposed approach and the proposed Glasgow Haskell Compiler modification by listing the disadvantages of alternatives. The secondary goal is to list alternative approaches to checked exceptions with their respective advantages and disadvantages for someone who cannot wait for the proposed Glasgow Haskell Compiler modification.
-
14:15–15:00
- Wed, 26.05.
-
14:30–14:40
Verification of Timed Automata with BDDs
BA Antrittsvortrag von Jingchen WangRaum: (online) Organisator: SoSy-Lab
-
14:30–14:40
- Fri, 21.05.
-
14:15–15:00
Bachelorarbeitsantrittsvortrag: Überblick über die Kategorientheorie und deren Anwendungen in der funktionalen Programmiersprache Haskell
von Denys KlypkinRaum: L109, Oettingenstr. 67 Organisator: TCSTalk details
Im Rahmen der Bachelorarbeit sollen die Grundlagen der Kategorientheorie aus Programmiersprachensicht erarbeitet und zusammenfassend dargestellt werden. Als wesentliche Grundlage und Ausgangspunkt soll dabei das Buch „Category Theory for Programmers“ von Bartosz Milewski dienen. Wesentliche Begriffe, welche in der Arbeit erläutert und durch Beispiele demonstriert werden sollen, sind Objekte und Pfeile, Kategorien, Morphismen, Produkte, Koprodukte, Funktoren, natürliche Transformationen, Adjunktion, das Lemma von Yoneda, die Yodena-Einbettung sowie Profunktor Optik. Auch Beispiele, welche das Zusammenspiel von Programmieren in Haskell und die Verwendung von Kategorientheorie unterstreichen, sind wünschenswert.
-
14:15–15:00
- Wed, 28.04.
-
14:30–14:55
Shareable Benchmarking Reports with Enhanced Filters and Dynamic Statistics for BenchExec
BA Abschlussvortrag von Dennis SimonRaum: (online) Organisator: SoSy-LabTalk details
BenchExec is a benchmarking tool developed at the Software and Computational Systems Lab of the Ludwig-Maximilians-Universität in Munich, Germany. One of its features is the automatic generation of a HTML table that presents the benchmarking results in an interactive and visual environment. The HTML table was recently rewritten in 2019 in the context of a bachelor thesis, with the performance and usability of the tables being greatly improved. This thesis showcases new sets of features that were built on top of this implementation and additionally showcases the integration of a rework of the filter functionality including the addition of a new global, more accessible user interface, the addition of multi-selection capabilities for status and category filters and components that allow a more granular filtering by task-ID. In order to improve user experience and to unlock shareability, navigation is now done via a "Hash Routing" approach, with most state, including filters, being serialized in the URL thus enabling the navigation history handling of the browser and allowing users to share state via a copied URL. To achieve a more consistent representation of the state of selected data, statistics that were previously statically included in the table are now asynchronously calculated using pooled web workers to reflect any changes in selected data that might occur by filtering. Lastly, the performance of the successful implementation is compared to the previous implementation. The changes described in this paper are already in use with some of them already being successfully extended further.
-
14:30–14:55
- Wed, 17.02.
-
14:30–14:55
Improve Analysis of Java Programs in CPAchecker
BA Abschlussvortrag von Sven MasardRaum: (online) Organisator: SoSy-LabTalk details
This bachelor thesis covers the adaptation and extension of CPAchecker in order to analyze a range of Java programs. A collection of Java programs used for the Competition on Software Verification exists that can be used to find and implement cases that CPAchecker was not yet able to handle. In order test this collection of Java programs with CPAchecker in one large batch, CPAchecker for Java is extended to accept property files which are passed using the benchmark definition files. Finally, a configurable program analysis to track exceptions inside of try catch statements is implemented and its implementation is evaluated by a short series of test programs.
-
14:30–14:55
- Wed, 10.02.
-
14:30–14:55
Converting between ACSL Annotations and Witness Invariants
BA Abschlussvortrag von Sven UmbrichtRaum: (online) Organisator: SoSy-LabTalk details
Proving the correctness of a given program with regard to a certain specification is hard. To make this task easier one can additionally give invariants that may aid the verification. Several formats exist to provide invariants for this purpose, like GraphML-based correctness witnesses or ACSL, but herein already lies the problem: A tool that relies on having invariants provided in a specific format cannot profit from invariants that are structured differently. It would therefore be helpful to be able to translate invariants from one format into the other. The goal of this thesis is to translate invariants from correctness witnesses into ACSL annotations and vice versa. We describe a possible way to perform these translations and implement a proof of concept in CPAchecker . Our evaluation shows that we can indeed generate valid ACSL-annotated programs from correctness witnesses produced by different verifiers and that we are able to again create valid witnesses for these annotated programs. -
15:15–15:40
Verification Witnesses: from Llvm to C
BA Abschlussvortrag von Yun ZhangRaum: (online) Organisator: SoSy-Lab
-
14:30–14:55
- Wed, 03.02.
-
12:30–13:00
Fuzzing/Legion in CPAchecker
MA Abschlussvortrag von Christoph GirstenbreiRaum: (online) Organisator: SoSy-Lab
-
12:30–13:00
- Wed, 27.01.
-
14:30–14:55
Implementierung und Evaluation von einfacher Schleifenabstraktion für das CPAchecker-Framework
BA Abschlussvortrag von Benedikt DamböckRaum: (online) Organisator: SoSy-LabTalk details
In der Programmverifikation haben viele Analysen Probleme mit komplizierten Schleifen. Es gibt jedoch die Option, diese zu abstrahieren, so dass die Analyse beschleunigt wird oder es sogar erst möglich wird, zu einem Ergebnis zu kommen. Bei dieser Arbeit handelt es sich um eine Reproduktion eines bestehenden Prinzips der Schleifenabstraktion. Dieses Prinzip wurde mit Anpassungen in das Verifikationprogramm CPAchecker integriert und mit Hilfe von Programmen getestet. Dabei wird es vor der normalen Analyse genutzt, um zu überprüfen, ob die Abstraktion von Schleifen im allgemeinen zu einer Leistungsverbesserung in den Kategorien Zeit und Speicherplatz führt. Es werden 3 SMT-basierte“ Analysen und die Value-Analyse, die ” Übersicht über konstante Variablenwerte behält, eingesetzt. -
15:30–15:40
Genetic Programming in Software Verification
BA Antrittsvortrag von Ludwig GlückstadtRaum: (online) Organisator: SoSy-LabTalk details
The idea is to generate verification tasks via genetic programming,i.e. do the following repeatedly on a set of programs:
1. mutation of the programs' ASTs
2. selection of 'fit' programs based by running the generated programs against some verifier and chosing some fitness metric that is determined by the verification resultsThis can then be used used for a large number of interesting applications:
One very simple would be fault localization: Here the allowed mutations are those that remove program statements, and the fitness is determined by a) the bug has to still be present and b) the shorter the program the fitter.
Another application would be to generate structure-wise simple programs that are still hard to solve or to generate programs that are easy to solve by verifier/approach A, but hard to solve by verifier/approach B.In the end the challenging part here (and why this probably has not been done really for software verification) is to keep time per roundtrip low enough to get enough iterations. For that the idea would be to start use bounded model checking/ limit the analysis time. Other tactics like speculative execution or using some static method to predict the fitness might also be worth exploring.
From a techical point of view the goal is to use BenchExec for executing the mutated programs each round (and such reduce the wall time for each round).
The language used for implementation will be Python3, which allows to use the pycparser as a frontend.
-
14:30–14:55
- Wed, 20.01.
- Fri, 15.01.
-
14:15–15:00
Variations and implementation details of Hopcroft's partitioning algorithm for DFA minimisation: Correctness and Time Complexity
von Elisabeth LempaRaum: zoom Organisator: TCSTalk details
In 1971, John Hopcroft described a new algorithm for DFA minimisation. This algorihm is claimed to run in O(m * n * log n) time (where n is the number of states and m is the size of the input alphabet), which is considerably faster than what was then viewed as the 'standard method', which requires O(n^2) steps. However, Hopcroft's original paper, being only five pages long, leaves out many implementation details that turn out to be crucial for achieving this runtime bound. This has of course led to a variety of other authors taking it upon themselves to fill in the gaps, coming up with wildly different approaches in the process. While the details of Hopcroft's initial algorithm were subsequently delivered in a textbook that Hopcroft co-authored and that was published three years later, this has not led people to stop trying to describe and modify the algorithm, with the most recent publication on the subject that I have yet discovered being from 2009. In this Masterarbeit, I will examine the different variations of the algorithm. A set of criteria will be given to discern if an algorithm can still be counted as a variation, or if it's a completely different algorithm. For what are deemed variations, the specific 'choice points' where the approaches differ will be described. And finally, software is used to make it possible to pick and choose which variation should be used at particular points, thereby allowing combination of details from different approaches and authors. It is then examined by testing which of these different combinations will a) give correct results, and b) meet the runtime bound.
-
14:15–15:00
- Wed, 13.01.
-
12:30–12:55
Converting Test Goals to Condition Automata
BA Abschlussvortrag von Frederic SchönbergerRaum: (online) Organisator: SoSy-Lab -
13:30–13:40
Taint Analysis for CPAchecker
BA Antrittsvortrag von Sebastian TschöpelRaum: (online) Organisator: SoSy-Lab -
13:50–14:00
Unityped functional programs and proofs
MA Antrittsvortrag von Lucas HoffmannRaum: (online) Organisator: SoSy-Lab -
14:10–14:20
Invariant Generation through Sampling for CPAchecker
BA Antrittsvortrag von Daniel MössnerRaum: (online) Organisator: SoSy-Lab
-
12:30–12:55
- Wed, 16.12.2020
-
12:30–12:55
Verification of Timed Automata with CPAchecker
MA Abschlussvortrag von Nico WeiseRaum: (online) Organisator: SoSy-LabTalk details
Automata are a formal model for systems of which the behavior is sensitive to time. Failures of such systems can have fatal consequences. Therefore, there is an interest to verify that such systems operate safely. To this end, a system can be modeled as timed automaton. The backbone of many of the state-of-the-art timed automaton verification tools are sophisticated data structures. Other tools use SMT-solvers. SMT-based methods express a verification problem as logical formulas, such that the verification problem is solvable by checking the satisfiability of these formulas. CPAchecker is a state-of-the-art software verification tool and implements SMT-based software verification. This thesis makes the first step towards timed automaton verification with CPAchecker by adding bounded model checking for reachability analyses of timed automata. Formula encodings are represented as composition of encoding parts. This makes it possible to reuse existing parts and define new encodings by configuration. The goal is to equip CPAchecker with a wide range of known encodings that are known to be efficient. An experimental evaluation of different encodings reveals that no encoding outperforms the others on every benchmark automaton. This result supports the idea to make a wide range of different encodings available by configuration, instead of explicitly implementing only some. A comparison with other tools shows that the implementation in CPAchecker is not yet sophisticated enough to be competitive. Moreover, the state-of-the-art tool Uppaal outperforms the bounded model checking approach on most of the benchmarks.
-
12:30–12:55
- Wed, 09.12.2020
-
12:30–12:55
Domain Types for Predicate Analysis in CPAchecker
BA Abschlussvortrag von Yannick AdamsRaum: (online) Organisator: SoSy-Lab -
13:30–13:55
SMT-based Model Checking of Concurrent Programs
BA Abschlussvortrag von Vladyslav KolesnykovRaum: (online) Organisator: SoSy-LabTalk details
Nowadays, modern software applications are complex concurrent and distributed software systems that should be highly reliable and efficient, without data races, deadlocks, and other program bugs. Thus, the automated verification of concurrent programs is becoming increasingly important in order to benefit from the potential of advanced multi-core hardware and distributed infrastructure. However, this process can be challenging even for modern verification software due to the non-deterministic behavior of multithreaded programs. Several successful automated software verification approaches are based on the Satisfiability Modulo Theories (SMT), solving first-order-logic formulas over predicates. This thesis studies two SMT-based software verification techniques, Bounded Model Checking and Predicate Abstraction, as well as a configurable verification framework CPAchecker for C programs. Our framework implements these approaches in a single configurable component for predicate-based analyses, representing Bounded Model Checking and Predicate Abstraction in a single setting. In addition to the theoretical contribution, we present our implementation that extends the existing components of CPAchecker to use Bounded Model Checking and Predicate Abstraction for concurrent programs. The predicate-based analyses component is used with the underlying reachability analysis that explores the program’s state-space analyzing all possible thread interleavings. We evaluate the performance of implemented verification techniques and some optimizations on the broad set of concurrent benchmark tasks, comparing them with other existing analyses in the same framework CPAchecker. We also present a combination of our techniques with explicit value-analysis to solve the state-space explosion problem and achieve even better verification performance. Finally, the implemented changes are applied as part of CPAchecker to participate in the International Competition on Software Verification 2021.
-
12:30–12:55
- Wed, 25.11.2020
- Wed, 18.11.2020
-
12:30–12:45
Domain-independent Function Summaries
MA Antrittsvortrag von Philipp WaldingerRaum: (online) Organisator: SoSy-Lab
-
12:30–12:45
- Wed, 11.11.2020
-
12:30–12:45
A Python Frontend for Cuvée
BA Antrittsvortrag von Maximilian DoodsRaum: (online) Organisator: SoSy-Lab
-
12:30–12:45
- Wed, 04.11.2020
- Wed, 21.10.2020
- Wed, 30.09.2020
-
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.2020
-
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.2020
-
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.2020
-
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.2020
-
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.2020
- Wed, 17.06.2020
- Wed, 10.06.2020
- Wed, 13.05.2020
-
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.2020
-
12:30–12:40
Fuzzing/Legion in CPAchecker
MA Antrittsvortrag von Christoph GirstenbreiRaum: (online) Organisator: SoSy-Lab
-
12:30–12:40
- Wed, 18.03.2020
-
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.2020
-
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.2020
-
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.2020
-
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.2020
-
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.2020
-
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.2020
-
12:30–13:00
Real-World Requirements for Software Analysis
BA Antrittsvortrag 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.2020
-
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.2020
-
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