Allgemein

A Systematic Approach to Deriving Incremental Type Checkers
André Pacak, Sebastian Erdweg, and Tamás Szabó,. In Proceedings of the ACM on Programming Languages (OOPSLA). ACM, 2020. [ pdf ]

Time: Friday, Feb 7, 10:00
Room: 03-233

Title: Modular Differential Software Verification and Pattern-based Equivalence Checking - Two Techniques for Incremental Verification

Abstract:
In this talk, I will give an overview on our current work in the area of incremental verification. The talk will consist of two parts. In the first part, I will present work in progress on modular differential software verification. Its basic idea is to restrict reverification to the modified program paths. I will explain how we identify the modified program paths and how we leverage conditional model checking to restrict verification to those modified program paths. In the second part, I will talk about our ideas on checking functional equivalence for parallelized program and how we want to make use of parallelization patterns.

Speaker bio:
Marie-Christine Jakobs is assistant professor at the TU Darmstadt leading the Semantics and Verification of parallel Systems group. She studied computer science at Paderborn University, where she also did her doctorate. From 2017 to 2019 she worked as postdoctoral researcher at LMU Munich. Her research focus is on theoretical results and practical approaches for automatic software verification. For example, she is one of the developers of the software verification framework CPAchecker. Currently, she is interested in incremental verification, the combination of verification approaches, test-case generation with verifiers, and the validation of verification results.

Time: Thursday, Jan 30, 14:00
Room: 03-424

Title: Riposte—A DSL for HTTP API black-box testing

Abstract:
Domain-specific languages are often made to solve a particular kind of problem in a particular time and place, with the hope is that others out there in the world have similar problems. In my case as a developer at an ecommerce shop, I was unsatisfied with the amount of testing our JSON-based HTTP APIs were getting. With the assumption that our tooling & language were to blame, I designed Riposte: an easy-to-read, fun-to-write functional language that allows one to write JSON, JSON Pointer, URI Templates in their respective surface syntaxes, and formulate HTTP requests in a straightforward way. Riposte programs are best understood as tests suites: one issues HTTP requests (possibly changing the state of a remote system) and makes assertions about values extracted from HTTP responses; the failure of an assertion causes the program to terminate. Riposte is implemented in Racket, a programming language that emphasizes language-oriented programming, making it especially useful for designing new languages. We present a little HTTP API and show how to test it in Riposte, discussing its syntax, semantics, and pragmatics along the way, along with a discussion of whether Riposte solved problem it set out to solve (answer: yes & no).

Speaker bio:
Jesse Alama is a full-stack developer at Vicampo.de. He earned his PhD at Stanford University working in interactive theorem proving & philosophy of mathematics, after which he worked as a postdoc in Lisbon and Vienna.

Time: Thursday, Dec 5, 14:00
Room: 03-424

Title: Static Analyses for Continuous Quality Improvement

Abstract:
As consultants for software and test quality, our goal is to support our customers in continuously improving the quality of their software systems. Considering the size and complexity of today’s software systems, this is only possible if we automate quality analysis to a point where we can quickly deliver an up-to-date overview on the quality of the system at any point in time. Developing such automated (static) analyses that are able to analyze large systems (incrementally) in close to real-time, however, is often quite challenging in itself. How we achieve this and which challenges we still face, is the topic of my talk.
Speaker bio:
Dr. Sven Amann is a software-quality consultant and developer at CQSE GmbH. He studied computer science at the Technische Universität Darmstadt (Germany) and the Pontifícia Universidade Católica do Rio de Janeiro (Brazil). He received his PhD in software technology from Technische Universität Darmstadt.

A Systematic Approach to Abstract Interpretation of Program Transformations.
Sven Keidel and Sebastian Erdweg. In Proceedings of International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, 2020. [ Details ]

Sound and Reusable Components for Abstract Interpretation
Sven Keidel and Sebastian Erdweg. In Proceedings of the ACM on Programming Languages (OOPSLA). ACM, 2019. [ Details ]

Language-Integrated Privacy-Aware Distributed Queries
Guido Salvaneschi, Mirko Köhler, Daniel Sokolowski, Philipp Haller, Sebastian Erdweg, and Mira Mezini. In Proceedings of the ACM on Programming Languages (OOPSLA). ACM, 2019. [ Details ]

Vision Paper: Generating Incremental Type Services
André Pacak and Sebastian Erdweg. In Proceedings of Software Language Engineering (SLE). ACM, 2019. [ Details ]

Prof. Dr. Friedrich Steimann from the Fern-Universität Hagen is visiting us July 9, 2019. He will give a guest lecture (in German) in our program analysis course (2:15pm in 05-426). Please find his title and abstract below.

Titel: Programmierwerkzeuge als Bedingungserfüllungsprobleme

Zusammenfassung:

Ein Bedingungserfüllungsproblem (engl. constraint satisfaction problem, CSP) besteht aus einer Menge von Variablen, jede mit einer Domäne von möglichen Werten, und einer Menge von Bedingungen (Constraints), die die Variablenbelegungen erfüllen müssen. Ein Bedingungserfüllungsproblem wird im Wesentlichen dadurch gelöst, dass für alle Variablen Werte gesucht werden, deren Zuweisung an die Variablen gleichzeitig alle Bedingungen erfüllen. Entsprechende Lösungsverfahren, Constraint Solver genannt, sind mittlerweile etabliert und gut verfügbar.

In dieser Vorlesung wird gezeigt, wie sich der Kern von Programmierwerkzeugen wie automatische Vervollständigung und Korrektur oder automatischen Refaktorisierungen auf Bedingungserfüllungsprobleme reduzieren lässt. Besondere Aufmerksamkeit gilt dabei der Gewinnung der Bedingungserfüllungsprobleme aus einer existierenden Spezifikation der statischen Semantik einer Programmiersprache und ihrer Anwendung auf ein Programm.

Sebastian Erdweg and his team move from TU Delft to JGU Mainz to start a new research group on programming languages.

Sebastian Erdweg joined the editorial board of the open-access Journal of Object Technology.