Student and Research Talks @ Sosy-Lab

Student and Research Talks at SoSy-Lab

Week View - Agenda View - Plain HTML - Download or Import ICal Feed

Wed, 06.12.
- 14:30–14:55
  Verification of Java Programs with Exceptions with CPAchecker
  
  Master-Thesis Final Talk von Benedikt Damböck
  Raum: F003 Organisator: SoSy-Lab
- 15:15–15:40
  Inferenz von Vorbedingungen für den Vergleich rekursiver Funktionen über ADTs
  
  Bachelor-Thesis Final Talk von Robin Sögtrop
  Raum: F003 Organisator: SoSy-Lab
- 16:00–16:15
  O2R: Reduction of No-Overflow Property of C Programs to Unreach-Call Property
  
  Bachelor-Thesis Introductory Talk von Xiyue Zheng (Mentor: Marek Jankola)
  Raum: F003 Organisator: SoSy-Lab

Past talks

Wed, 29.11.
- 14:30–14:55
  Case Studies in the Dynamic Logic of Communicating Hybrid Programs
  
  Bachelor-Thesis Final Talk von Aileen Chen
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Due to cyber-physical systems (CPS) being safety-critical, their verification is highly important. Parallel CPS can be modelled as communicating hybrid programs (CHP). Dynamic logic of communicating hybrid programs dLCHP is a logic specifically for modelling and verifying CHP. The challenge of their verification lies within the communication and parallelism aspect. To evaluate the expressiveness and deductive power of dLCHP , this bachelor thesis focuses on two case studies (Vehicle Cruise Control and Adaptive Cruise Control). Modelling the case studies and expressing the models more naturally in dLCHP works very well. Not only can the parallel components be verified separately, but the communication aspect is also part of the logic itself and therefore integrated into the verification process. Hence, conducting the case studies manually using sequent calculus, turned out to be feasible, even without a theorem prover. Though manual verification is a little time-consuming, given that the original Adaptive Cruise Control would have required quite a few case distinctions, an automated proof using Keymaera X [4] could prove helpful. The latter, however, was not in scope of this bachelor thesis.
- 15:00–15:25
  Scaling Formal Verification: Parallel Analysis of Functions in CPAchecker
  
  Bachelor-Thesis Final Talk von Jens Linden
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  A problem that hinders proper applicability of static analyzers in the industry, is the time needed for analysis on big code bases. The goal of this work is to achieve a faster availability of the verification verdict in CPAchecker through parallel computation. This is aimed to make the tool more attractive in industrial use cases in which time should be used as efficiently as possible. Facebook’s tool Infer intro- duces a concept to make static analyzers more applicable in industry, their tool is used as reference for this work. With this work a sim- ilar approach as that of Infer is implemented in the framework of CPAchecker. We use a divide and conquer approach to decompose the analysis task and analyze the smaller tasks domain-independent in parallel. The input program will be divided by function calls and the resulting blocks are then analyzed in parallel. This leads to a faster availability of the analysis results. Additionally, a list of all errors that were found in the analysis run with their corresponding information of the program path and variable values that are needed to reach the error (stack traces) will be provided. This new approach is also compared with Infer on the SV-COMP benchmark set 2023. That is possible because of prior work of configuring Infer for SV- COMP (Infer-sv). Also the analysis method that is used by Infer, Symbolic Execution, was added as configurable option for the new introduced approach in CPAchecker. As shown in the evaluation our approach provides an 85.5% decrease in wall time consumption for the trade off an increased amount of false positives opposed to CPAchecker. The results also showed that our approach has a 45.0% increased wall time consumption opposed to Infer-sv.
Wed, 22.11.
- 14:30–14:55
  Certifying Software Violation Witnesses for Hardware Verification Tasks via Simulation-Based Validation
  
  Bachelor-Thesis Final Talk von Nils Sirrenberg
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Previous studies have proven that software verifiers are able to uniquely find bugs in digital hardware circuits, which traditional hardware model checkers don't detect. Necessary for this is only the previous translation of the hardware circuit to a C program using the tool Btor2C. In this thesis, the translation in the opposite way is realized, from the software violation witness to the hardware witness in Btor2 format. This facilitates the usage of Software verifiers in combination with these two translators as black box hardware verifier for violation witnesses, with Btor2 circuits as input and Btor2 witnesses as output.Using additional validation of the generated Btor2 witness by a simulation-based validation approach, the verification result is certified, resulting in increased trust into the result and the error path described in the violation witnesses.
- 15:10–15:20
  Verification of Micro Services Based on Pact API Contracts
  
  Bachelor-Thesis Introductory Talk von Robin Mattis
  Raum: F003 Organisator: SoSy-Lab
Wed, 08.11.
- 14:30–14:55
  Detection of Performance Deviation in CPAchecker Using Microbenchmarking
  
  Bachelor's Thesis Defense Talk von Josef Feger (Mentor: Martin Spiessl)
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Executing a CPAchecker analysis with a known result and runtime using BenchExec in a new environment, can unexpectedly lead to, for example, a different runtime, if the new system’s performance has a great enough difference compared to the baseline system. In a worst case, this may cause the analysis to run into a timeout, if the performance difference is big enough, the baseline analysis was already close to hitting the time limit and the time limit was not changed by the user. This work focuses on researching whether it is possible to accurately measure a system’s performance, by expanding CPAchecker’s functionality to include benchmarking capability, and notify the user of a potential deviation from a baseline performance.
- 15:00–15:15
  T2R: Reduction of Termination of C programs to Reachability-Safety Problem
  
  Bachelor-Thesis Introductory Talk von Tian Xia (Mentor: Marek Jankola)
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  TBA
- 15:15–15:40
  Adding the SMT Solver Bitwuzla to the JavaSMT Framework and Evaluation using CPAchecker
  
  Bachelor's Thesis Defense Talk von Heinrich Lindner (Mentor: Daniel Baier)
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Adding the SMT solver Bitwuzla to the JavaSMT framework allows its users to utilize a powerfull solver spezialized in Bitvectors and Floats. The evaluation using CPAchecker uses multiple different solvers on the BMC algorithm to compare their capabilities.
Tue, 31.10.
- 11:00–11:15
  Test Algorithm Selection via Boolean Features
  
  Bachelor-Thesis Introductory Talk von Khrystyna Reichel (Mentor: Marie-Christine Jakobs)
  Raum: F003 Organisator: SoSy-Lab
Wed, 18.10.
- 14:30–14:45
  Adding Assertions for Undefined Behavior to Programs
  
  Bachelor-Thesis Introductory Talk von Karim Triki (Mentor: Thomas Lemberger)
  Raum: F003 Organisator: SoSy-Lab
Mon, 16.10.
- 10:00–10:30
  Adding the SMT Solver OpenSMT2 to the JavaSMT Framework and subsequent Evaluation
  
  Bachelor-Thesis Final Talk von Daniel Raffler (Mentor: Daniel Baier)
  Raum: F003 Organisator: SoSy-Lab
Wed, 11.10.
- 14:30–14:45
  Verification of Java Micro-Services based on OpenAPI
  
  Master-Thesis Introductory Talk von Daniel Bilic (Mentor: Thomas Lemberger)
  Raum: F003 Organisator: SoSy-Lab
- 15:00–15:15
  Building a Unit-Verification Library
  
  Bachelor-Thesis Introductory Talk von Marko Ristic (Mentor: Thomas Lemberger)
  Raum: F003 Organisator: SoSy-Lab
Wed, 20.09.
- 14:30–14:50
  Synthesizing a GUI for CoVeriTeam from its Source Code
  
  Bachelor-Thesis Defense Talk von Jasmin Krenz
  Raum: F003 Organisator: SoSy-Lab
- 15:15–15:30
  Adding Assertions for Undefined Behavior to Programs
  
  Bachelor-Thesis Introductory Talk von Karim Triki
  Raum: F003 Organisator: SoSy-Lab
Wed, 30.08.
- 14:30–14:55
  Improving the Encoding of Arrays in Btor2-to-C Translation
  
  Bachelor-Thesis Defense Talk von Salih Ates
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Btor2C is a tool that translates word-level Btor2 circuits into C programs, enabling software verifiers to handle hardware verification tasks. However, it also reveals a weakness of software verifiers in dealing with Btor2 circuits involving array sorts. None of the evaluated software verifiers found proof for these Btor2 verification tasks. To address this issue, we have developed two solutions. The first solution blasts the arrays in a Btor2 circuit into sequences of bit-vectors and simulates operations for arrays with bit-vector operations. The solution is implemented as a standalone script and can be used as a preprocessor before Btor2C. The second solution is an enhancement to Btor2C, which creates an optimal ordering of intermediate circuit nodes to schedule writing operations to arrays as late as possible. Based on this optimal scheduling, we can minimize the number of duplicates needed for writing operations. Both solutions have effectively increased the number of verified Btor2 tasks with arrays overall.
- 15:00–15:25
  Designing and Assessing a Benchmark Set for Fault Localization Using Fault Injection
  
  Bachelor-Thesis Defense Talk von Moritz Bierwirth
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  With the further development of communication systems, which are becoming increasingly complex, the number of faults in the software of these systems is also rising. To be able to keep up with this growth, fault localization techniques are becoming increasingly important. Researchers or research groups proposing a new technique for fault localization usually evaluate it on programs with known faults. The main goal of our approach is to create a benchmark set, that can be used to evaluate these techniques. We achieve this goal by creating V-FIT, Verified Fault Injection Tool. It combines the two verifiers CPAchecker and UAutomizer to verify a given subset of safety tasks from the SV-COMP benchmark set and includes the fault injection tool Coccinelle to inject the faults. V-FIT verifies each file after injection again and creates a new fault localization benchmark set, consisting of a sensible folder structure and for each injected fault a metadata file and two files specifying the fault and the exact location. Furthermore, we evaluate the fault localization benchmark set by doing a quantitative analysis to show the performance of V-FIT and a qualitative analysis to examine the weaknesses and strengths of the created benchmark set. In total, V-FIT only processed 3 percent of the subset of tasks from the SV-COMP benchmark set successfully, but nevertheless, a total of 858 fault injections were created and thus a basis for further work was created.
Wed, 23.08.
- 14:30–14:55
  Using Time-Independent Resource Limits to Improve the Reproducibility of CPAchecker
  
  Bachelor-Thesis Defense Talk von Ludwig Dinter
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Resource limits are essential in static software verification research for practical reasons, avoiding excessive resource usage. But they can also be a source for indeterminism, threatening the replicability of verification results. This holds true especially for timedependent limits such as CPU time. Replicability is highly desirable in the fields of science and software testing. Therefore, we suggest time-independent limits as an alternative, which are based on statistics metrics provided by the static software verification tool CPAchecker. We call these statistic limits. We implemented statistics limit in CPAchecker in two different ways, global- and task-wise. Specifically, a statistics limit called iteration limit, which refers to iterations of the main CPAchecker algorithm, has been investigated with respect to the two implementations. We have evaluated the implications of time-independent limits for the task set integration-nightly-value included in CPAchecker. Generally, it is shown that the iteration limit improves the replicability of verification results. However, due to a lack of linear correlation with the CPU time, it is not guaranteed to be intuitive to use in the global implementation. The task-wise implementation mitigates this issue at the cost of requiring two verification runs to achieve replicable results. This research can be extended to include other analyses than value analysis, building on the statistics limit implementation provided in this thesis.
Wed, 02.08.
- 13:00–13:30
  How Good Are Your Invariants: Witness Validation for Hardware via Circuit Instrumentation with Software Invariants
  
  Internship final talk von Zsófi Ádám, BME, Hungary
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Zsófi is an internship student from BME, Hungary. During the last two months, she has been working on translating software correctness witnesses back to hardware for Btor2C programs. The focus in these witnesses is on the invariants, so the quality of invariants also became an important factor. Thus this talk will include not just the instrumentation of Btor2 circuits with invariants, but also different checks for validation, proving different qualities of the invariant and the current state of SV-COMP correctness witnesses for Btor2C programs.
Tue, 25.07.
- 13:30–13:40
  Differential Fuzzing with AFL and JQF
  
  Bachelor-Thesis Introductory Talk von Marta Gołaszewska
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  TBD
Wed, 19.07.
- 14:30–14:55
  Learning Systems as Automata with Unbounded State Space
  
  BA Abschlussvortrag von Bastian Beuttel
  Raum: F003 Organisator: SoSy-Lab
Wed, 12.07.
- 14:30–14:55
  Ethik-basierte Anforderungsanalyse für eine Triage-Software: eine Fallstudie
  
  BA Abschlussvortrag von Dusica Weisbarth
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Ein Thema, welches durch die COVID-19 Pandemie ins Rampenlicht gestellt wurde, ist die Triage, d.h. die Priorisierung von Patienten bei Leistung medizinischer Hilfe. Als Lösung zur Entlastung der Ärzte bei solchen Entscheidungen wird eine KI-gestützte Software vorgeschlagen.
  Das Ziel dieser Bachelorarbeit ist es, eine Anforderungsanalyse für eine solche Triage-Software durchzuführen, deren Ergebnis zur Formulierung von weiteren Richtlinien genutzt werden könnte.
  Zu Beginn geht der Theorieteil dieser Arbeit auf die Grundlagen der Ethik, sowohl im Bereich Medizin, als auch der Informatik, ein. Im Medizinteil wird sich vorwiegend auf die Triage konzentriert. Der Informatikteil stellt zwei ausgewählte Ansätze der Softwareentwicklung (Ethik- und Werte-basiert) vor und zeigt am Beispiel von Codes of Conduct (CoCs) warum die dadurch entstandenen Richtlinien nicht ausreichend sind.
  Als Antwort auf die Unzulänglichkeit bisheriger Richtlinien wird dann das EDAP-Shema vorgestellt, welches die Grundlage für die Anforderungsanalyse bildet. Diese Analyse beinhaltet das Abwägen von derzeitigen gesetzlichen Regelungen für Triage im deutschsprachigen Raum, ethische Fragen, denen man sich stellen muss, und ethische Vorgaben, die bei der Entwicklung einer Triage-Software in Erwägung gezogen werden sollten.
  Der Kern der Anforderungsanalyse ist eine Fallstudie, in der die Stakeholder (Informatiker, Mediziner und Personen aus der allgemeinen Bevölkerung) Fragen zu ihren ethischen Ansichten, ihren Sorgen und ihren Werten beantworten, die auf die Entwicklung einer Ethik-basierten Triage-Software hinzielen. Die Studie soll sicherstellen, dass die Bedürfnisse der Stakeholder in der Anforderungsanalyse angemessen berücksichtigt werden. Die Ergebnisse der Studie dienen zur Verfeinerung der Anforderungsanalyse, bzw. der Aktualisierung des EDAP-Schemas.
- 15:00–15:10
  Violation Witness Translation from C to Btor2
  
  Bachelor-thesis introductory talk von Nils Sirrenberg
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Btor2 is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C is a hardware-to-software translator that converts circuits in Btor2 format to C programs. With Btor2C, one could analyze hardware designs with off-the-shelf software verifiers. If a software verifier finds an error in the program, it generates a violation witness, which records the execution path leading to that error. The goal of this project to translate the violation witnesses in GraphML format produced by software verifiers to Btor2 format, such that one could use hardware simulators to validate them.
Fri, 07.07.
- 11:00–11:30
  Experiments with Rapidly-exploring Random Trees over Trajectories
  
  Research Talk von Jiří Fejlek
  Raum: F003/hybrid Organisator: SoSy-Lab
- 13:00–13:25
  Updating the BenchExec Core Assignment for Modern CPU Architecture
  
  BA Abschlussvortrag von Charlotte Gall
  Raum: (online) Organisator: SoSy-Lab
  Talk details
  Performance requirements demand that processors get faster and manufacturers get creativ on how to satisfy the ever increasing need for computing power. The result is that over the last years, a new generation of processors was released. Their topology became quite complex and variable, with additional architectural elements as well as the trend to use memory regions with non-uniform memory access (NUMA). Benchmarking is a common technique to evaluate tools and software programs. To get reliable results from the parallel benchmarking runs, the benchmarking framework has to minimize interferance between parallel runs. The benchmarking framework BenchExec aims to meet this challenge with the principle of locality: each execution run gets specific cores assigned, that are close together and far away from other execution runs and cannot be used otherwise. To keep up with the changes of development and innovation, this thesis updates the current core allocation algorithm to include system information on the more modern elements in processor architecture during the core assignment process. Even though first evaluation results show only slight improvements, the proposed core allocation algorithm may provide more convincing results for benchmarks with higher memory requirements.
Wed, 05.07.
- 13:00–13:30
  Test Interference Detection for C Projects
  
  Student talk von Florian Eder
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  During test execution, automated software tests can interfere, i.e., their results can deviate depending on their (possibly interleaved) execution order. Such interference imposes severe restrictions on regression testing, when execution order is not or cannot be controlled for, as they can lead to non-deterministic deviations of test results giving false indication of regressions in the code base. While the phenomenon has been extensively studied for Java and Python projects, it remains unclear if or how the obtained results apply for other languages with different practices of test organization and execution. Our study contributes to filling that gap by reporting results from a large-scale study on test interference in 134 C projects. In total, we identify test interference in 13 projects. In order to efficiently detect interferences, we propose and evaluate different test execution strategies with varying trade-offs between the number of test executions and their potential for interference detection. As these strategies are specific to the resources that tests interfere on, rather than the language in which the code is written, we expect them to be useful for the study of test interference in other languages as well.
- 14:30–14:40
  Formal Verification of Interactive Visual Novels
  
  MA Antrittsvortrag von Elisabeth Lempa
  Raum: F003 Organisator: SoSy-Lab
- 14:50–15:00
  Security Specifications for Dafny
  
  MA Antrittsvortrag von Maximilian Doods
  Raum: F003 Organisator: SoSy-Lab
Tue, 04.07.
- 11:00–12:00
  Theta Tool Introduction and Validation-via-Verification for Hardware Btor2 Circuits
  
  Student talk von Zsófi Ádám, BME, Hungary
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Zsófi is a visiting student from BME, Hungary. In this talk, she will first give an introduction on Theta, a configurable model checking framework developed at her group, and her Master thesis topic on trace generation. Then, she will talk about the research project "Validation-via-Verification for Hardware Btor2 Circuits" that she is currently working on during her stay at SoSy-Lab.
- 14:00–14:45
  Threats to Reproducibility in Software Engineering
  
  Habil Antrittsvortrag von Stefan Winter
  Raum: F003 Organisator: Stefan Winter
  Talk details
  The creation of reproducible results is a core concern for every scientific discipline. While many disciplines have been reported to face a "reproducibility crisis" over the last decade, the investigation of these phenomena has mostly focused on the health and social sciences rather than engineering disciplines. On that basis, the 2019 NASEM report "Reproducibility and Replicability in Science" (https://doi.org/10.17226/25303) identified several common threats to the reproducibility and replicability in science, which are mostly pertaining to the availability of research artifacts. Software engineering, however, has a long-standing tradition of "artifact evaluations", i.e., a systematic assessment of the digital objects involved in scientific publications, This makes software engineering and interesting field of study for reproducibility, as it can help to reveal potential threats to reproducibility, once the availability of research artifacts has been addressed. In my talk I will present insights from my previous and ongoing work on identifying and mitigating threats to reproducibility in software engineering, focusing on (a) limitations of existing artifact evaluation practices to ensure reproducibility and (b) volatile software executions, which lead to non-deterministic and irreproducible results.
Thu, 29.06.
- 11:00–12:00
  Data-Driven Formal Methods: Oxymoron or Panacea?
  
  Invited talk von Raphael Jungers, UCLouvain, Belgium
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  In formal methods, there has been a recent surge of interest for the design of symbolic controllers that would be obtained 'ab nihilo', from the sole observation of data harvested from the system, without the help of a mathematical model. The observed data would allow to build an abstraction of the actual system, in such a way that a controller designed for the abstraction would automatically be valid for the actual system. If the industrial motivations are obvious and promising, the question of whether such a technology is possible at all is still not well understood. In short, what type of formal guarantees can we give about a system which is known only through a finite number of observations?
  In recent years, some partial answers have been obtained: among others, the scenario approach and interval markov decision processes have provided tools that partly allow to reconcile this oxymoron: one can indeed learn the system from data, in a monte-carlo fashion, and provide statistical guarantees on the quality of the abstraction. In this talk, I'll first survey these recent breakthroughs. Then I'll depart from that approach (by assuming that the monte-carlo sampling provides infinite accuracy), and will investigate another challenge inherent with data-driven abstractions: these techniques implicitly make an assumption of Markovianity, which may be violated on the true system. I will show how this assumption can ruin the approach if improperly handled, and will propose ways to mitigate and control the induced error, by leveraging concepts from ergodic theory, symbolic dynamics, and probability theory.
  Biography:
  Raphael Jungers is a Professor at UCLouvain, Belgium, currently on sabbatical leave at Oxford University. His main interests lie in the fields of Computer Science, Graph Theory, Optimization and Control. He received a Ph.D. in Mathematical Engineering from UCLouvain (2008), and a M.Sc. in Applied Mathematics, both from the Ecole Centrale Paris, (2004), and from UCLouvain (2005).
  He has held various invited positions, at the Université Libre de Bruxelles (2008-2009), at the Laboratory for Information and Decision Systems of the Massachusetts Institute of Technology (2009-2010), at the University of L´Aquila (2011, 2013, 2016), and at the University of California Los Angeles (2016-2017).
  He is a FNRS, BAEF, and Fulbright fellow. He has been an Editor at large for the IEEE CDC, Associate Editor for the IEEE CSS Conference Editorial Board, and the journals NAHS (2015-2016; Senior Editor 2023-), Systems and Control Letters (2016-2017), IEEE Transactions on Automatic Control (2015-2020), Automatica (2020-). He was the recipient of the IBM Belgium 2009 award and a finalist of the ERCIM Cor Baayen award 2011. He was the co-recipient of the SICON best paper award 2013-2014, the HSCC2020 best paper award, and an ERC 2019 laureate.
Wed, 28.06.
- 13:00–14:00
  Omitting types theorem in hybrid dynamic first-order logic with rigid symbols
  
  Invited talk von Guillermo Badia, University of Queensland
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  In the present contribution, we prove an Omitting Types Theorem (OTT) for an arbitrary fragment of hybrid dynamic first-order logic with rigid symbols (i.e. symbols with fixed interpretations across worlds) closed under negation and retrieve. The logical framework can be regarded as a parameter and it is instantiated by some well-known hybrid and/or dynamic logics from the literature. We develop a forcing technique and then we study a forcing property based on local satisfiability, which lead to a refined proof of the OTT. For uncountable signatures, the result requires compactness, while for countable signatures, compactness is not necessary. We apply the OTT to obtain upwards and downwards Löwenheim-Skolem theorems for our logic, as well as a completeness theorem for its constructor-based variant.
- 14:15–14:25
  Implementing a solver-independent SMTLIB2 parser und generator for JavaSMT with subsequent evaluation
  
  Bachelor-thesis introductory talk von Janelle King
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  JavaSMT offers a common API layer for multiple SMT solvers. However, JavaSMT only supports solver that themselfs offer a public API. Since many solvers do not do this, we want to develop a SMT-LIB2 parser and generator interface, able to connect to all SMT-LIB2 solvers. To proof the parser/generator correct, we want to evaluate the new components of the JavaSMT framework.
- 14:30–14:40
  Scaling Formal Verification: Parallel Analysis of Functions in CPAchecker
  
  BA Antrittsvortrag von Jens Linden
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Verifying complex programs with respect to a given specification (e.g., 'check that function reach_error is never called') may be time consuming. To make verifiers more applicable in industry, we want to tackle the problem with a divide-and-conquer approach. We decompose the verification task in multiple smaller tasks that are then verified in parallel. As soon as one of the analyses reports a violation, we abort all other analyses and report the violation. This will lead to many false alarms since we do not know with which input parameters functions will be called. Return values of functions will be ignored and interpreted as unknown value in a first step. From there we can continue in two directions:
  1. Analyze functions under a user defined condition (e.g., a user restricts the values of parameter x of function foo to the interval [0;100])
  2. We identify each function call automatically and try to infer all parameters.
  Finally, we will evaluate this approach on the SV-COMP benchmark set. This topic is inspired by the tool Infer.
Tue, 27.06.
- 17:00–17:10
  Extending the Framework JavaSMT with the Apron Library for Abstract Numeric Domains with subsequent Evaluation using CPAchecker
  
  BA Antrittsvortrag von Winnie Ros
  Raum: F003 Organisator: SoSy-Lab
Wed, 21.06.
- 14:30–14:40
  Extending the Framework JavaSMT with the Apron Library for Abstract Numeric Domains with subsequent Evaluation using CPAchecker
  
  BA Antrittsvortrag von Winnie Ros
  Raum: F003 Organisator: SoSy-Lab
- 14:50–15:15
  Changes of flakiness in a combined test suite
  
  BA Abschlussvortrag von Lorenz Leithäuser
  Raum: F003 Organisator: SoSy-Lab
Wed, 14.06.
- 13:00–13:40
  SafeSens: A systematic approach for determining safety-related limitations of perception architectures under consideration of uncertainty
  
  Doc Antrittsvortrag von Iwo Kurzidem, Fraunhofer IKS
  Raum: F003 Organisator: SoSy-Lab
- 14:45–14:55
  Supporting the family of scanf functions in CPAchecker
  
  BA Antrittsvortrag von Nils Sirrenberg
  Raum: F003 Organisator: SoSy-Lab
Wed, 31.05.
- 14:30–15:00
  A Framework for Sampling-Based Invariant Generation
  
  MA Abschlussvortrag von Sven Umbricht
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  The task of finding suitable invariants for a given loop is one of the main problems of automatic software verification and as such many potential ways of generating invariants have been investigated. In recent years, many approaches have been proposed that use samples -potential assignments of the program variables- to infer invariants, rather than working with the program directly. This thesis aims to simplify research of sampling-based loop invariant inference approaches by introducing a modular framework that separates the actual invariant generation from the collection of samples and invariant validation, thus allowing to reuse common components for new techniques. The presented framework makes it possible to compare different invariant generation approaches more fairly and combine them to leverage complementing strengths.
- 15:15–15:25
  Inferring loop summaries with quantifiers over arrays
  
  BA Antrittsvortrag von Hannah Knie
  Raum: F003 Organisator: SoSy-Lab
- 15:30–15:40
  Verification of Java Programs with Exceptions with CPAchecker
  
  MA Antrittsvortrag von Benedikt Damböck
  Raum: F003 Organisator: SoSy-Lab
- 15:45–15:55
  Synthesizing a GUI for CoVeriTeam from its source code
  
  BA Antrittsvortrag von Jasmin Krenz
  Raum: F003 Organisator: SoSy-Lab
Wed, 17.05.
- 14:30–14:40
  Implementing a solver-independent SMTLIB2 parser und composer for JavaSMT with subsequent evaluation
  
  Bachelor-thesis introductory talk von Janelle King
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  JavaSMT offers a common API layer for multiple SMT solvers. However, JavaSMT only supports solver that themselfs offer a public API. Since many solvers do not do this, we want to develop a SMT-LIB2 parser and composer interface, able to connect to all SMT-LIB2 solvers. To proof the parser/composer correct, we want to evaluate the new components of the JavaSMT framework.
Wed, 03.05.
- 14:30–14:40
  Improving the Encoding of Arrays in Btor2-to-C Translation
  
  Bachelor-thesis introductory talk von Salih Ates
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  The publication about Btor2C has shown that software verifiers had difficulties verifying C programs translated from Btor2 models with arrays. This thesis aims to improve how arrays are encoded in the Btor2-to-C translation flow by exploring two directions: (1) blasting arrays into sequences of bit-vectors and (2) avoiding unnecessary duplications when writing values to arrays. The goals are to speed up the verification process and increase the number of proofs for the translated C programs.
- 14:45–14:55
  Extending the SMT solver framework JavaSMT with Bitwuzla
  
  Bachelor-thesis introductory talk von Heinrich Lindner
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  JavaSMT offers a common API layer for multiple SMT solvers. Extending the available solvers boosts the versatility of JavaSMT and offers more options for users. Bitwuzla, the successor of Boolector, is an SMT solver that offers strong Bitvector support and in general more support for features, such as the computation of unsatisfiable cores of formulas.
Wed, 15.03.
- 14:40–14:50
  Adding support for OpenSMT2 to the JavaSMT Framework
  
  BA Antrittsvortrag von Daniel Raffler
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  The JavaSMT framework provides users with a common API for several SMT solvers. This thesis extends this framework with the SMT solver OpenSMT2. OpenSMT2 offers several theories and features, such as interpolation. The final implementation will be tested with automated tests and evaluated against already implemented SMT solvers in JavaSMT using the CPAchecker framework.
- 14:45–14:55
  CPAchecker Result Reproducibility Through Micro Benchmarking
  
  BA Antrittsvortrag von Josef Feger
  Raum: F003 Organisator: SoSy-Lab
  Talk details
  Running verification benchmarks with known results on an unknown hardware may lead to unexpected results, such as time outs because of slower hardware. This work focuses on trying to mitigate this effect by looking into micro benchmarks and how they can be used in the CPAchecker environment to reproduce previous verification benchmark results on unknown hardware or to at least notify the user about large performance differences compared to the base line hardware.
Thu, 09.02.
- 11:00–11:30
  Fuzzing Strategies and Optimization in Legion/SymCC
  
  BA Abschlussvortrag von Lukas Ederer
  Raum: (online) Organisator: SoSy-Lab
Wed, 01.02.
- 14:30–14:40
  Updating the BenchExec Core Assignment for Modern CPU Architectures
  
  BA Antrittsvortrag von Charlotte Gall
  Raum: (online) Organisator: SoSy-Lab
Wed, 18.01.
- 14:30–14:40
  Improving Resource Limits for CPAchecker
  
  BA Antrittsvortrag von Ludwig Dinter
  Raum: (online) Organisator: SoSy-Lab
Wed, 19.10.2022
- 14:30–14:40
  A Framework for Invariant Learning in Software Verification
  
  MA Antrittsvortrag von Sven Umbricht
  Raum: (online) Organisator: SoSy-Lab
  Talk details
  The task of finding suitable invariants for a given loop is one of the main problems of automatic software verification and as such many potential ways of generating invariants have been investigated. One such approach that tries to make use of recent advances in machine learning is one that is based on sampling. Sampled variable assignments of the program variables are used to train a classifier to distinguish between program states that fulfill an unknown loop invariant and those that do not. The learned decision boundary may be treated as the desired invariant for the purpose of program verification and can be refined by adding more samples.
  Whether a sufficiently strong invariant can be learned this way in a reasonable amount of time depends on the choice of both the learning algorithm and the algorithm used for collecting and selecting samples. The goal of this thesis is thus to investigate and compare different approaches for collecting samples from a given program as well as ways for generating invariants from a set of samples. Based one our findings, sampling-based invariant generation shall be implemented in CPAchecker and compared with the current search-based analysis.
Wed, 28.09.2022
- 14:30–14:50
  Prevalence and Structure of External Validity Discussions in FSE Articles
  
  BA Abschlussvortrag von Benedikt Wiederrecht
  Raum: (online) Organisator: SoSy-Lab
  Talk details
  External validity discussions concern the question of the extent to which results can be generalized, i.e., transferred to other contexts. The question arises on how to properly discuss external validity in software engineering research. Previously, Sjøberg [22] and Siegmund [21], among others, have dealt with threats to validity (internal and external validity discussions) in empirical software engineering research, and did not find a consensus among researchers on how to deal with threats to validity. This thesis in a sense continues that work by examining external validity discussions in articles from the ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) between 2019 and 2021. I conduct a systematic literature review of all articles from FSE 2019 to 2021, that are at least ten pages long, and investigate each article’s external validity discussion for pro and contra arguments. By then applying ”Open Card Sorting,” I assign labels to argument types that occur frequently across the FSE articles examined. This work pursues three goals: (1) present the current status on external validity discussions in recent FSE articles, (2) demonstrate how the study type (experimental, empirical and case study) influences the existence of external validity discussions and (3) to elaborate and discuss the authors’ most common arguments regarding the generalizability of results. I find a total of 64% of all examined FSE articles to include an external validity discussion. The largest proportion of papers that have an external validity is accounted for by empirical papers (papers based on an observation) with 84%. Experimental papers (based on a manipulation/intervention by the researcher) have an external validity discussion in 56% of the cases and case studies (study subjects bound to study environment) 62%. Last, the most common discussed threats to external validity are selection bias, not applicable to different contexts and the representativeness of the dataset.
- 15:15–15:35
  Consistency Assessment for Publication Metadata
  
  BA Abschlussvortrag von Elhassan Ould El Moustapha
  Raum: (online) Organisator: SoSy-Lab
  Talk details
  The goal of this thesis is to assess the consistency of publication metadata. In order to achieve this goal a uniform schema has been developed that allows the comparison of metadata from different metadata providers and their schemas. Additionally, a webtool has been created that executes API requests, highlights discrepancies and provides more relevant information. A study including numerous researchers of a research group working in computer science has been conducted, to investigate what types of discrepancies there are, how frequently they appear and if there is a relation between the discrepancy type and the metadata provider.
- 16:00–16:30
  Implementation of Value Analysis over Symbolic Memory Graphs in CPAchecker
  
  MA Abschlussvortrag von Daniel Baier
  Raum: (online) Organisator: SoSy-Lab
  Talk details
  Concrete-value analysis is a software verification technique that uses concretely known values in programs to analyze them. It is independant of an external solver and has been successfully extended by the techniques CEGAR and interpolation to improve upon its results. Despite the simplicity of the value analysis, it is up to this day performing well in the ongoing competitions on software verification. However, the analysis lacks the ability to track memory and memory operations accurately and is therefore not able to analyze memory safety properties of a program or analyse programs with a heap memory in general. Symbolic memory graphs (SMGs) are a successful approach to model and abstract memory in order to analyze memory-safety related issues in programs. This thesis extends the domain of concrete-value analysis with SMGs and refines the resulting software analysis using a CEGAR approach. Besides tracking the complete memory of a program closely enough to analyze memory-safety, concrete values in memory structures are also tracked by SMGs. CEGAR is used to track only necessary program variables, avoiding the problem of state-space-explosion in many cases. Furthermore, this thesis focuses on abstraction with linked lists using the technique of SMGs. The abstraction of linked lists not only reduces the resources needed by the analysis of lists, but also enables the analysis to verify programs with large lists. CEGAR is again used to improve upon this by tracking only values necessary to prove or refute a violation. Also, the type of the list used to abstract lists is refined, again based on the needs of the analysis. The resulting analysis is capable of tracking all the memory of a program and analyse programs based on it. The analysis is implemented in the CPACHECKER framework, and is subsequently tested using the benchmarking tool BENCHEXEC. The tests are run using subsets of benchmarks for memory-safety and reach-safety that are both used in the international competition on soft ware verification 2022. Furthermore, the results for reach-safety are evaluated against the state-of-the-art value analysis of CPACHECKER , whilst the results for memory-safety are evaluated against PREDATORHP, a comparable memory analysis tool that also uses SMGs and no background solver. While the results in the reach-safety category outperformed the state-of-the-art value analysis in regards to heap memory tasks, problems held back the new analysis, especially in tasks related to memory allocation with non-concrete values. These problems could be identified as a weakness of the combination of value analysis with CEGAR and SMGs. Also, the results showed that the analysis could not outperform PREDATORHP, while still solving the majority of memory-safety tasks correctly.
Wed, 31.08.2022
- 14:30–15:00
  A New Spin on Verification with Symbolic Execution: Symbolic Execution as Formula-Based Predicate Analysis in CPAchecker
  
  MA Abschlussvortrag von Martin Pletl
  Raum: (online) Organisator: SoSy-Lab
- 15:15–15:45
  Prevalence and Structure of External Validity Discussions in Experimental and Empirical Software Engineering Research
  
  BA Abschlussvortrag von Emine Hakani
  Raum: (online) Organisator: SoSy-Lab
- 16:00–16:15
  Predicting the future of CPAchecker tests
  
  BA Antrittsvortrag von Thai Le
  Raum: (online) Organisator: SoSy-Lab
Wed, 27.07.2022
- 14:30–15:00
  Juristische und technische Betrachtung von IT-Sicherheit bei Cloud Computing
  
  BA Abschlussvortrag von Johannes Eykman
  Raum: (online) Organisator: SoSy-Lab
  Talk details
  The aim of this work is to clarify the question of whether security vulnerabilities in a cloud computing service offering of a cloud service provider (CSP) constitute a defect (cf. 1.1 Problem Outline). For this purpose, selected literature in computer science and law was consulted in the form of a secondary research approach (cf. 1.4 Scientific Methodology). The thesis combines technical elements (cf. 2 Cloud Computing) and elements of security (cf. 3 IT Security) with legal elements (cf. 4 Cloud Computing Contracts) in order to be able to derive a security law view (cf. 5 Security Law View of B2B Cloud Computing 5 Contracts). The results of this consideration are only applicable to business to business (B2B) relationships, which is why consumer contracts are treated separately (cf. 6 Consumer contracts in cloud computing). Whether a service of a CSP is defective depends on several factors of the individual case. Consequently, no generally valid answer to the research question can be given (cf. 5.1 Security gaps as defects). Accordingly, the rights and obligations of contract participants in connection with IT security cannot be universally classified. The main reason for this is that rights and obligations can regularly be changed by individual contract design and by the use of general terms and conditions (cf. 5.2, 5.3). To enable a uniform approach, a definition of IT security was drawn up from the approaches in the specialist literature considered (cf. 3.1.3 Definition) as well as a definition of security vulnerabilities (cf. 3.3.1 Definition). To establish security according to this definition, a security model is regularly developed, on the basis of which providers take measures oriented to the required security level. These measures are divided into the three areas of technical, organizational and physical IT security (cf. 3.2 Three pillars of IT security). In principle, cloud computing contracts in the B2B area are typologized as rental contracts, in individual cases also as service or work contracts. The creation and, depending on the type of contract, maintenance of security of the service is a central contractual obligation of the CSP within the framework of the respective applicable security level (cf. 4.4 Tenancy Law). Limits of this obligation lie in particular in the state of the art, which represents a technical feasibility barrier for the measures, as well as in the economic feasibility of security (cf. 5.2.2 Limits of the obligations). On the other hand, the customer has, in addition to the payment of the agreed remuneration, the obligation to take the rights and interests of the CSP sufficiently into consideration and, in case of an occurring damage, to minimize or avert it (cf. 5.3 Security Responsibilities of the Customer). In light of the newly introduced regulations of §§ 327 et seq. BGB, an adapted approach to cloud contracts in the business to consumer (B2C) area is necessary. These are now to be typified uniformly as service contracts. The warranty law added by the new regulations can be applied to them in the event of poor performance. (cf. 6.2 New contract typology and new concept of defects). Since §§ 327 et seq. BGB are not directly applicable to B2B contracts and not by analogy, these contracts still have to be typologized as described in 4.3. Only in the case of 6 gaps in B2B contracts the new regulations can gain importance by way of supplementary contract interpretation in conformity with European law by the courts (cf. 6.4 Outlook and Influence on B2B Contracts). Due to the mention of security in the wording of §§ 327 et seq. BGB, this is given a high priority, which clearly expresses the expectations of the legislator for providers and the associated economy (cf. 6.5 IT security in consumer contracts).
Wed, 20.07.2022
- 14:30–15:00
  Program Transformation in CPAchecker: Design and Implementation of a Source-Respecting Translation from Control-Flow Automata to C Code
  
  BA Abschlussvortrag von Klara Cimbalnik
  Raum: (online) Organisator: SoSy-Lab
Wed, 15.06.2022
- 14:30–15:00
  New Approaches and Visualization for Verification Coverage
  
  MA Abschlussvortrag von Maximilian Hailer
  Raum: (online) Organisator: SoSy-Lab
Wed, 11.05.2022
- 14:30–14:40
  Technische und juristische Betrachtung von IT-Sicherheit bei XaaS
  
  BA Antrittsvortrag von Johannes Eykman
  Raum: (online) Organisator: SoSy-Lab
Wed, 30.03.2022
- 14:30–14:40
  Prevalence and Structure of External Validity Discussions in Experimental and Empirical Software Engineering Research
  
  BA Antrittsvortrag von Emine Hakani
  Raum: (online) Organisator: SoSy-Lab
- 14:45–14:55
  Order-Dependent Flaky Test Analysis for C Programs
  
  BA Antrittsvortrag von Florian Eder
  Raum: (online) Organisator: SoSy-Lab
Wed, 16.03.2022
- 14:30–14:55
  Developing a Verifier Based on Parallel Portfolio with CoVeriTeam
  
  BA Abschlussvortrag von Tobias Kleinert
  Raum: (online) Organisator: SoSy-Lab
Wed, 09.03.2022
- 14:15–14:25
  Impact of Mutation Operators on Defect Detection
  
  BA Antrittsvortrag von Sophia Hans
  Raum: (online) Organisator: SoSy-Lab
- 14:30–14:55
  A CPA for String Analysis for Java Programs in CPAchecker
  
  BA Abschlussvortrag von Simon Antonischki
  Raum: (online) Organisator: SoSy-Lab
- 14:30–14:55
  Cgroups v2 Support for BenchExec
  
  BA Abschlussvortrag von Robin Gloster
  Raum: (online) Organisator: SoSy-Lab
Thu, 24.02.2022
- 09:00–09:35
  Adjustable Block Analysis: Actor-Based Creation of Block Summaries for Scaling Formal Verification
  
  MA Abschlussvortrag von Matthias Kettl
  Raum: (online) Organisator: SoSy-Lab
Wed, 23.02.2022
- 14:30–14:50
  Idiom Mining for Software Verification
  
  MA Antrittsvortrag von Valentin Port
  Raum: (online) Organisator: SoSy-Lab
Wed, 16.02.2022
- 14:30–14:50
  Staying true to the original in the face of change: Comprehensible code transformation
  
  BA Antrittsvortrag von Klara Cimbalnik
  Raum: (online) Organisator: SoSy-Lab
Wed, 09.02.2022
- 14:30–15:05
  Concurrent Software Verification through Block-based Task Partitioning and Continuous Summary Refinement
  
  MA Abschlussvortrag von Philipp Waldinger
  Raum: (online) Organisator: SoSy-Lab
Wed, 02.02.2022
- 14:30–14:50
  Integration of Symbolic Execution into Predicate Analysis
  
  MA Antrittsvortrag von Martin Pletl
  Raum: (online) Organisator: SoSy-Lab
Wed, 19.01.2022
- 14:30–14:50
  SMG Analysis in CPAchecker
  
  MA Antrittsvortrag von Daniel Baier
  Raum: (online) Organisator: SoSy-Lab
Wed, 22.12.2021
- 14:30–14:50
  SMG Analysis in CPAchecker
  
  MA Antrittsvortrag von Daniel Baier
  Raum: (online) Organisator: SoSy-Lab
Wed, 10.11.2021
- 14:30–14:50
  New Approaches and Visualization for Verification Coverage
  
  MA Antrittsvortrag von Maximilian Hailer
  Raum: (online) Organisator: SoSy-Lab
- 14:50–15:25
  SV-COMP Benchmarks for Weak Memory Models
  
  BA Abschlussvortrag von Korab Zogu
  Raum: (online) Organisator: SoSy-Lab
  Talk 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ückstadt
  Raum: (online) Organisator: SoSy-Lab
  Talk 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.
Wed, 03.11.2021
- 15:00–15:45
  Effcient Software Model Checking with Block-Abstraction Memoization
  
  Disputation von Karlheinz Friedberger
  Raum: Hauptgebäude A120 and online via Zoom Organisator: SoSy-Lab
  Talk 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.
Wed, 20.10.2021
- 14:30–15:00
  Iterated Prisoner's Dilemma with Players Learning to Provide Unpaid and Paid Incentives to Others
  
  BA Abschlussvortrag von Xiyue Sun
  Raum: (online) Organisator: SoSy-Lab
- 15:00–15:30
  Linear Interpolation of Multiple Objectives
  
  BA Abschlussvortrag von Mario Quitt
  Raum: (online) Organisator: SoSy-Lab
- 15:30–16:00
  Leveraging Curricula to Explore Pareto Fronts in Multi-Objective Reinforcement Learning
  
  BA Abschlussvortrag von Philip Adamczyk
  Raum: (online) Organisator: SoSy-Lab
Wed, 13.10.2021
- 14:30–15:05
  CWE-Ids for Software Analysis in CPAchecker
  
  BA Abschlussvortrag von Clara Sofie Goldmann
  Raum: (online) Organisator: SoSy-Lab
  Talk 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.
Wed, 22.09.2021
- 14:30–15:05
  Implementation and Evaluation of tagged BDDs in PJBDD
  
  BA Abschlussvortrag von Simon Raths
  Raum: (online) Organisator: SoSy-Lab
- 15:15–15:30
  Adjustable Block Analysis: Actor-based block summaries for scaling formal verification
  
  MA Antrittsvortrag von Matthias Kettl
  Raum: (online) Organisator: SoSy-Lab
Wed, 28.07.2021
- 14:30–14:40
  A CPA for String Analysis for Java Programs in CPAchecker
  
  BA Antrittsvortrag von Simon Antonischki
  Raum: (online) Organisator: SoSy-Lab
- 14:50–15:00
  Use cgroups v2 for BenchExec to improve container isolation
  
  BA Antrittsvortrag von Robin Gloster
  Raum: (online) Organisator: SoSy-Lab
- 15:10–15:35
  Implementation and Evaluation of a Simple Taint Analysis for CPAchecker
  
  BA Abschlussvortrag von Robin Gloster
  Raum: (online) Organisator: SoSy-Lab
Fri, 11.06.2021
- 14:15–15:00
  Antrittsvortrag Bachelorarbeit: Codierung und Decodierung von Faltungscodes durch deterministische Transduktoren
  
  von Johannes Schlüßlhuber
  Raum: L109, Oettingenstr. 67 Organisator: TCS
  Talk 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 Ganz
  Raum: L109, Oettingenstr. 67 Organisator: TCS
  Talk 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.
Fri, 28.05.2021
- 14:15–15:00
  Checked Exceptions for Haskell
  
  von Philipp Zander
  Raum: L109, Oettingenstr. 67 Organisator: TCS
  Talk 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.
Wed, 26.05.2021
- 14:30–14:40
  Verification of Timed Automata with BDDs
  
  BA Antrittsvortrag von Jingchen Wang
  Raum: (online) Organisator: SoSy-Lab
Fri, 21.05.2021
- 14:15–15:00
  Bachelorarbeitsantrittsvortrag: Überblick über die Kategorientheorie und deren Anwendungen in der funktionalen Programmiersprache Haskell
  
  von Denys Klypkin
  Raum: L109, Oettingenstr. 67 Organisator: TCS
  Talk 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.
Wed, 28.04.2021
- 14:30–14:55
  Shareable Benchmarking Reports with Enhanced Filters and Dynamic Statistics for BenchExec
  
  BA Abschlussvortrag von Dennis Simon
  Raum: (online) Organisator: SoSy-Lab
  Talk 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.
Wed, 17.02.2021
- 14:30–14:55
  Improve Analysis of Java Programs in CPAchecker
  
  BA Abschlussvortrag von Sven Masard
  Raum: (online) Organisator: SoSy-Lab
  Talk 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.
Wed, 10.02.2021
- 14:30–14:55
  Converting between ACSL Annotations and Witness Invariants
  
  BA Abschlussvortrag von Sven Umbricht
  Raum: (online) Organisator: SoSy-Lab
  Talk 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 Zhang
  Raum: (online) Organisator: SoSy-Lab
Wed, 03.02.2021
- 12:30–13:00
  Fuzzing/Legion in CPAchecker
  
  MA Abschlussvortrag von Christoph Girstenbrei
  Raum: (online) Organisator: SoSy-Lab
Wed, 27.01.2021
- 14:30–14:55
  Implementierung und Evaluation von einfacher Schleifenabstraktion für das CPAchecker-Framework
  
  BA Abschlussvortrag von Benedikt Damböck
  Raum: (online) Organisator: SoSy-Lab
  Talk 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ückstadt
  Raum: (online) Organisator: SoSy-Lab
  Talk 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 results
  This 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.
Wed, 20.01.2021
- 12:30–12:55
  Information Flow Testing of a PGP Key Server
  
  BA Abschlussvortrag von Lukas Rieger
  Raum: (online) Organisator: SoSy-Lab
- 13:15–13:40
  SMT-based Checking and Synthesis of Formal Refinements
  
  MA Abschlussvortrag von Tillmann Gaida
  Raum: (online) Organisator: SoSy-Lab
Fri, 15.01.2021
- 14:15–15:00
  Variations and implementation details of Hopcroft's partitioning algorithm for DFA minimisation: Correctness and Time Complexity
  
  von Elisabeth Lempa
  Raum: zoom Organisator: TCS
  Talk 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.
Wed, 13.01.2021
- 12:30–12:55
  Converting Test Goals to Condition Automata
  
  BA Abschlussvortrag von Frederic Schönberger
  Raum: (online) Organisator: SoSy-Lab
- 13:30–13:40
  Taint Analysis for CPAchecker
  
  BA Antrittsvortrag von Sebastian Tschöpel
  Raum: (online) Organisator: SoSy-Lab
- 13:50–14:00
  Unityped functional programs and proofs
  
  MA Antrittsvortrag von Lucas Hoffmann
  Raum: (online) Organisator: SoSy-Lab
- 14:10–14:20
  Invariant Generation through Sampling for CPAchecker
  
  BA Antrittsvortrag von Daniel Mössner
  Raum: (online) Organisator: SoSy-Lab
Wed, 16.12.2020
- 12:30–12:55
  Verification of Timed Automata with CPAchecker
  
  MA Abschlussvortrag von Nico Weise
  Raum: (online) Organisator: SoSy-Lab
  Talk 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.
Wed, 09.12.2020
- 12:30–12:55
  Domain Types for Predicate Analysis in CPAchecker
  
  BA Abschlussvortrag von Yannick Adams
  Raum: (online) Organisator: SoSy-Lab
- 13:30–13:55
  SMT-based Model Checking of Concurrent Programs
  
  BA Abschlussvortrag von Vladyslav Kolesnykov
  Raum: (online) Organisator: SoSy-Lab
  Talk 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.
Wed, 25.11.2020
- 12:30–12:55
  Fuzzing with CMA-ES
  
  BA Abschlussvortrag von Hyunsung Kim
  Raum: (online) Organisator: SoSy-Lab
- 13:30–13:55
  Software Verification with Numerical Domains in CPAchecker
  
  BA Abschlussvortrag von Martin Zehendner
  Raum: (online) Organisator: SoSy-Lab
Wed, 18.11.2020
- 12:30–12:45
  Domain-independent Function Summaries
  
  MA Antrittsvortrag von Philipp Waldinger
  Raum: (online) Organisator: SoSy-Lab
Wed, 11.11.2020
- 12:30–12:45
  A Python Frontend for Cuvée
  
  BA Antrittsvortrag von Maximilian Doods
  Raum: (online) Organisator: SoSy-Lab
Wed, 04.11.2020
- 12:30–13:00
  Real-World Requirements for Software Analysis
  
  BA Abschlussvortrag von Amena Abdulla
  Raum: (online) Organisator: SoSy-Lab
- 13:45–13:55
  Verification Witnesses: from Llvm to C
  
  BA Antrittsvortrag von Yun Zhang
  Raum: (online) Organisator: SoSy-Lab
Wed, 21.10.2020
- 12:30–13:00
  Test-Harness Generation with Non-deterministic Pointers
  
  BA Abschlussvortrag von Jakob Selberg
  Raum: (online) Organisator: SoSy-Lab
- 13:20–13:50
  Code-complexity analysis on the component level
  
  BA Abschlussvortrag von Simon Lund
  Raum: (online) Organisator: SoSy-Lab
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 Kafounis
  Raum: (online) Organisator: SoSy-Lab
- 13:20–13:50
  For The Win (FTW) Agent
  
  Abschlussvortrag Praktikum zur Entwicklung eines groesseren Softwaresystems von Johannes Tochtermann
  Raum: (online) Organisator: SoSy-Lab
- 14:15–14:45
  Integration und Evaluation von verketteten Entscheidungsdiagrammen in PJBDD und CPAchecker
  
  BA Abschlussvortrag von Sebastian Niedner
  Raum: (online) Organisator: SoSy-Lab
Wed, 16.09.2020
- 12:30–12:40
  CWE-IDs for Software Analysis in CPAchecker and SV-COMP
  
  BA Antrittsvortrag von Clara Goldmann
  Raum: (online) Organisator: SoSy-Lab
- 12:50–13:20
  Interval-based Optimization for SMT Solvers
  
  BA Abschlussvortrag von Radu Rusanu
  Raum: (online) Organisator: SoSy-Lab
  Talk 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 Beck
  Raum: (online) Organisator: SoSy-Lab
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 Ali
  Raum: (online) Organisator: SoSy-Lab
Wed, 22.07.2020
- 12:30–13:15
  Fault Localization in CPAchecker with Error Invariants and UNSAT-Cores
  
  BA Abschlussvortrag von Matthias Kettl
  Raum: (online) Organisator: SoSy-Lab
- 13:15–14:00
  Energy Consumption Prediction of Verification Work
  
  BA Abschlussvortrag von Petros Isaakidis
  Raum: (online) Organisator: SoSy-Lab
  Talk 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.
Wed, 15.07.2020
- 12:30–12:40
  A Booge Frontend for Cuvee
  
  BA Antrittsvortrag von Marius Funk
  Raum: (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ünchow
  Raum: (online) Organisator: SoSy-Lab
- 13:30–14:15
  An IDE Plugin for CPAchecker
  
  BA Abschlussvortrag von Adrian Leimeister
  Raum: (online) Organisator: SoSy-Lab
Wed, 01.07.2020
- 12:30–12:45
  Interactive Verification Debugging in VS Code
  
  MA Antrittsvortrag von Johannes Blau
  Raum: (online) Organisator: SoSy-Lab
- 13:00–13:15
  Kombination der ThreadingCPA mit SMT-basierter Analyse
  
  BA Antrittsvortrag von Vladyslav Kolesnykov
  Raum: (online) Organisator: SoSy-Lab
Wed, 17.06.2020
- 12:30–12:45
  Fuzzing with Stochastic Optimization
  
  BA Antrittsvortrag von Hyunsung Kim
  Raum: (online) Organisator: SoSy-Lab
- 12:45–13:00
  Converting Test Goals to Condition Automata
  
  BA Antrittsvortrag von Frederic Schoenberger
  Raum: (online) Organisator: SoSy-Lab
Wed, 10.06.2020
- 12:30–12:40
  Interval-based Optimization for SMT Solvers
  
  BA Antrittsvortrag von Radu Rusanu
  Raum: (online) Organisator: SoSy-Lab
- 12:45–13:30
  Implementation of interpolation-based model checking in CPAchecker
  
  PhD Project Presentation von Nian-Ze Lee
  Raum: (online) Organisator: SoSy-Lab
Wed, 13.05.2020
- 12:30–13:15
  Extending the Framework JavaSMT with the SMT Solver Yices2
  
  BA Abschlussvortrag von Michael Obermeier
  Raum: (online) Organisator: SoSy-Lab
  Talk 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 Lund
  Raum: (online) Organisator: SoSy-Lab
- 13:30–13:45
  Support for Invariant Annotations from Correctness Witnesses in CPAchecker
  
  BA Antrittsvortrag von Sven Umbricht
  Raum: (online) Organisator: SoSy-Lab
Wed, 06.05.2020
- 12:30–12:40
  Fuzzing/Legion in CPAchecker
  
  MA Antrittsvortrag von Christoph Girstenbrei
  Raum: (online) Organisator: SoSy-Lab
Wed, 18.03.2020
- 12:30–13:15
  Loop Contracts for Boogie and Dafny
  
  Masterprojekt Abschlusspraesentation von Johannes Blau
  Raum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
Wed, 11.03.2020
- 13:00–13:10
  Fault Localization with Tarantula
  
  BA Antrittsvortrag von Schindar Ali
  Raum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
  Talk 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.
Fri, 06.03.2020
- 14:15–15:00
  BDD-unterstützes SAT-Solving
  
  BA Abschlussvortrag von Florian Leimgruber
  Raum: L109, Oettingenstr. 67 Organisator: TCS
  Talk 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.
Wed, 12.02.2020
- 12:30–13:00
  SMT-based checking and synthesis of formal refinements
  
  MA Antrittsvortrag von Tillmann Gaida
  Raum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
Wed, 05.02.2020
- 12:30–12:40
  Improve usability of summary tab for HTML tables of BenchExec
  
  BA Antrittsvortrag von Dennis Simon
  Raum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
Wed, 29.01.2020
- 12:30–13:15
  Rely/Guarantee for Separation Logic in SecC
  
  Masterprojekt Abschlusspraesentation von Bernhard Pöttinger
  Raum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
- 13:30–14:00
  Fault Localization with Error Invariants
  
  BA Antrittsvortrag von Matthias Kettl
  Raum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
  Talk 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 Ried
  Raum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
  Talk 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.
Wed, 22.01.2020
- 12:30–13:00
  Real-World Requirements for Software Analysis
  
  BA Antrittsvortrag von Amena Abdalla
  Raum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
- 13:15–13:45
  Information Flow Testing für ein Modell eines PGP Servers
  
  BA Antrittsvortrag von Lukas Rieger
  Raum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
Tue, 14.01.2020
- 10:00–10:30
  Octagon Analysis in CPAchecker (with ELINA)
  
  BA Antrittsvortrag von Martin Zehendner
  Raum: F003, Oettingenstr. 67 Organisator: SoSy-Lab
Thu, 09.01.2020
- 14:15–15:00
  Unifikation von Multimengengleichungen von Variablen-zu-Variablen-Bindungen
  
  BA Abschlussvortrag von Taro Yoshioka
  Raum: L109, Oettingenstr. 67 Organisator: TCS
  Talk 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.

Student and Research Talks at SoSy-Lab

Verification of Java Programs with Exceptions with CPAchecker

Inferenz von Vorbedingungen für den Vergleich rekursiver Funktionen über ADTs

O2R: Reduction of No-Overflow Property of C Programs to Unreach-Call Property

Case Studies in the Dynamic Logic of Communicating Hybrid Programs

Scaling Formal Verification: Parallel Analysis of Functions in CPAchecker

Certifying Software Violation Witnesses for Hardware Verification Tasks via Simulation-Based Validation

Verification of Micro Services Based on Pact API Contracts

Detection of Performance Deviation in CPAchecker Using Microbenchmarking

T2R: Reduction of Termination of C programs to Reachability-Safety Problem

Adding the SMT Solver Bitwuzla to the JavaSMT Framework and Evaluation using CPAchecker

Test Algorithm Selection via Boolean Features

Adding Assertions for Undefined Behavior to Programs

Adding the SMT Solver OpenSMT2 to the JavaSMT Framework and subsequent Evaluation

Verification of Java Micro-Services based on OpenAPI

Building a Unit-Verification Library

Synthesizing a GUI for CoVeriTeam from its Source Code

Adding Assertions for Undefined Behavior to Programs

Improving the Encoding of Arrays in Btor2-to-C Translation

Designing and Assessing a Benchmark Set for Fault Localization Using Fault Injection

Using Time-Independent Resource Limits to Improve the Reproducibility of CPAchecker

How Good Are Your Invariants: Witness Validation for Hardware via Circuit Instrumentation with Software Invariants

Differential Fuzzing with AFL and JQF

Learning Systems as Automata with Unbounded State Space

Ethik-basierte Anforderungsanalyse für eine Triage-Software: eine Fallstudie

Violation Witness Translation from C to Btor2

Experiments with Rapidly-exploring Random Trees over Trajectories

Updating the BenchExec Core Assignment for Modern CPU Architecture

Test Interference Detection for C Projects

Formal Verification of Interactive Visual Novels

Security Specifications for Dafny

Theta Tool Introduction and Validation-via-Verification for Hardware Btor2 Circuits

Threats to Reproducibility in Software Engineering

Data-Driven Formal Methods: Oxymoron or Panacea?

Omitting types theorem in hybrid dynamic first-order logic with rigid symbols

Implementing a solver-independent SMTLIB2 parser und generator for JavaSMT with subsequent evaluation

Scaling Formal Verification: Parallel Analysis of Functions in CPAchecker

Extending the Framework JavaSMT with the Apron Library for Abstract Numeric Domains with subsequent Evaluation using CPAchecker

Extending the Framework JavaSMT with the Apron Library for Abstract Numeric Domains with subsequent Evaluation using CPAchecker

Changes of flakiness in a combined test suite

SafeSens: A systematic approach for determining safety-related limitations of perception architectures under consideration of uncertainty

Supporting the family of scanf functions in CPAchecker

A Framework for Sampling-Based Invariant Generation

Inferring loop summaries with quantifiers over arrays

Verification of Java Programs with Exceptions with CPAchecker

Synthesizing a GUI for CoVeriTeam from its source code

Implementing a solver-independent SMTLIB2 parser und composer for JavaSMT with subsequent evaluation

Improving the Encoding of Arrays in Btor2-to-C Translation

Extending the SMT solver framework JavaSMT with Bitwuzla

Adding support for OpenSMT2 to the JavaSMT Framework

CPAchecker Result Reproducibility Through Micro Benchmarking

Fuzzing Strategies and Optimization in Legion/SymCC

Updating the BenchExec Core Assignment for Modern CPU Architectures

Improving Resource Limits for CPAchecker

A Framework for Invariant Learning in Software Verification

Prevalence and Structure of External Validity Discussions in FSE Articles

Consistency Assessment for Publication Metadata

Implementation of Value Analysis over Symbolic Memory Graphs in CPAchecker

A New Spin on Verification with Symbolic Execution: Symbolic Execution as Formula-Based Predicate Analysis in CPAchecker

Prevalence and Structure of External Validity Discussions in Experimental and Empirical Software Engineering Research

Predicting the future of CPAchecker tests

Juristische und technische Betrachtung von IT-Sicherheit bei Cloud Computing

Program Transformation in CPAchecker: Design and Implementation of a Source-Respecting Translation from Control-Flow Automata to C Code

New Approaches and Visualization for Verification Coverage

Technische und juristische Betrachtung von IT-Sicherheit bei XaaS

Prevalence and Structure of External Validity Discussions in Experimental and Empirical Software Engineering Research

Order-Dependent Flaky Test Analysis for C Programs

Developing a Verifier Based on Parallel Portfolio with CoVeriTeam

Impact of Mutation Operators on Defect Detection

A CPA for String Analysis for Java Programs in CPAchecker

Cgroups v2 Support for BenchExec

Adjustable Block Analysis: Actor-Based Creation of Block Summaries for Scaling Formal Verification

Idiom Mining for Software Verification

Staying true to the original in the face of change: Comprehensible code transformation

Concurrent Software Verification through Block-based Task Partitioning and Continuous Summary Refinement

Integration of Symbolic Execution into Predicate Analysis

SMG Analysis in CPAchecker

SMG Analysis in CPAchecker

New Approaches and Visualization for Verification Coverage

SV-COMP Benchmarks for Weak Memory Models