update of the abstracts

Author: wadoon

config.yml

@@ -17,6 +17,8 @@ persons:
   "Joshua Bachmeier":
     mail: "[email protected]"
     link: ""
+  "Dirk Beyer":
+    link: "https://www.sosy-lab.org/people/beyer/"
   "Bernhard Beckert":
     mail: "[email protected]"
     link: "https://formal.iti.kit.edu/beckert"

talks/beyer.md

@@ -2,9 +2,12 @@
 author: "Dirk Beyer"
 kind: "Invited Talk"
 track: "Common Track"
-title: "tbd"
+title: "Distributed Automatic Contract Construction"
 slot:  207
 length: 60
 type: invited
 order: 70
 ---
+
+
+The presentation consists of two parts. The first part presents an approach to automatic contract construction that is more modular, scalable, and precise compared to existing automatic approaches. We decompose the program into code blocks, and for each code block, we compute a postcondition and a violation condition. The postcondition of a block is given to successors in order to refine their precondition and derive a proof of correctness. The violation condition is a condition that describes states leading to a specification violation. The approach is scalable because each block can be analyzed independently: the blocks communicate only via postconditions and violation conditions. The precision of the approach can be defined by the underlying program analysis. In a second part, we describe an approach to conserve tools for formal methods. We collect and maintain essential data about tools for formal methods in a central repository, called FM-Tools, available at https://gitlab.com/sosy-lab/benchmarking/fm-tools. The repository contains metadata, such as which tools are available, which versions are advertized for each tool, and what command-line arguments to use for default usage. The actual tool executables are stored in tool archives at Zenodo, and for technically deep documentation, references point to archived publications or project web sites. With this approach, we can conserve today's tools for the future.

talks/graetz.md

@@ -8,11 +8,10 @@ length: 30
 order: 62
 ---
 
+More than 15 years ago, a paper ""Better bug reporting with better privacy"" solved the two problems of automatic bug reports: Specifically, memory dumps might not be sufficient to reconstruct an issue/crash while leaking private information. However, their approach of generating new input-data had limited applicability.
 
-More than 15 years ago, a paper "Better bug reporting with better privacy" solved the two problems of automatic bug reports: Specifically, memory dumps might not be sufficient to reconstruct an issue/crash while leaking private information.
+Our tool instruments the source code to record (with low overhead) a compressed control flow trace, which can be directly added to a bug-report (instead of input-data or memory dumps). The trace format is designed to be adaptable to different programming languages.
 
-In this talk, we will follow a related approach with improved overhead and portability: Our tool instruments the source code to record (with low overhead) a compressed control flow trace, which can be directly added to a bug-report. The trace format is designed to be adaptable to different programming languages.
+In the second part, these traces are used not only by visualizing the control-flow in the code: On the developers side, we can debug a trace using symbolic execution (we call that retracing). Our current implementation works on top of either KeY, CBMC or angr.
 
-In the second part, we see what a developer can do with these traces apart from visualizing in the source code: We use symbolic execution to retrace (partial program run reconstruction), to inspect variable values and to check against specifications/assertions. Our current implementation works on top of either KeY, CBMC or angr.
-
-We also see how to record a trace with KeY, useful for debugging a KeY-proof and restricting it to a single control flow (and then retrying, i.e., with different proof strategy settings).
+We also see how to record a trace with KeY and how to restrict symbolic execution (or a part of it) to a single control flow, to avoid loop invariants and path explosion.

talks/heydari-tabar.md

@@ -2,9 +2,12 @@
 author: "Asmae Heydari-Tabar"
 kind: "Short Talk (10 min. + 5 min.)"
 track: "Common Track, KeY-only Track"
-title: "Data Dependence Logic: Applications"
+title: "Data Dependence Analysis Program Logic: Applications"
 slot: 209
 length: 15
 order: 71
 ---
 
+
+We developed a program logic and a sequent calculus to formally address the data dependence analysis problem in high-performance computing. This program logic is rich and powerful enough to be used in different contexts when the problem at hand can be formulated in terms of data dependences. In this presentation, we briefly discuss such problems (e.g., method contract generation, noninterference verification, branch prediction, etc.).
+

talks/kern.md

@@ -2,9 +2,24 @@
 author: "Philipp Kern"
 kind: "Regular Talk (20 min. + 10 min.)"
 track: "Common Track, KeY-only Track"
-title: "TBD: Sth about NN Verification (probably verification of LSTMs)"
+title: "Towards Precise Linear Relaxations for Verification of LSTMs"
 length: 30
 slot: 32
 order: 104
 ---
 
+Verification of neural networks is essential for their deployment in
+safety-critical applications. While most verification approaches target
+ReLU networks, the activation functions used in Long Short-Term Memory
+(LSTM) networks, crucial for sequence and time series data, still pose
+significant challenges.
+
+Existing approaches for verification of LSTMs neglect dependencies
+between input variables, when computing linear relaxations of their
+activation functions.
+
+In this talk, I am going to present ongoing work for enhancing the
+precision of the linear relaxations by leveraging zonotopes to capture
+such input dependencies.
+
+