TU BRAUNSCHWEIG

Alexander Knüppel, M.Sc.

Institut für Softwaretechnik und Fahrzeuginformatik
Technische Universität Braunschweig

Informatikzentrum
Mühlenpfordtstr. 23
38106 Braunschweig

Raum: IZ 412
Sprechstunde: Nach Vereinbarung

Tel. +49 531 391-2289

Email: a.knueppel[at]tu-bs.de
ResearchGate

Forschungsschwerpunkte

  • Feature-oriented software development (FOSD)
  • Software Produktlinien (SPLs) und Analyse
  • Feature-Modellierung
  • Formale Methoden/Formale Verifikation: Deduktive Verifikation, Model Checking, Type Systems, statische Analyse, Assertion checking
  • Formale Spezifikation: Design by Contracts (DbC), Z-Notation, B-Method
  • Theorembeweisen mit Coq

Aktivitäten

Projekte

  • (CCC: Controlling Concurrent Change)

Lehre

Sommersemester 2018

Wintersemester 2017/2018

Sommersemester 2017

Wintersemester 2016/2017

  • Teamprojekt: Plugin-Entwicklung mit Eclipse (Organisation)

Sommersemester 2016

Aktuell angebotene studentische Arbeiten:

Schaut bitte hier nach: aktuelle Abschlussarbeiten. Bei Interesse einfach melden.

Betreute Studentische Arbeiten

Veröffentlichungen

2018

  • Alexander Knüppel, Carsten Pardylla, Thomas Thüm, and Ina Schaefer. Experience Report on Formally Verifying Parts of OpenJDK's API with KeY. In Fourth Workshop on Formal Integrated Development Environment (F-IDE), July 2018. To appear.
    Deductive verification of software has not yet found its way into industry, as complexity and scalability issues require highly specialized experts. The long-time perspective is, however, to develop verification tools aiding industrial software developers to find bugs or bottlenecks in software systems faster and more easily. The KeY project constitutes a framework for specifying and verifying software systems, aiming at making formal verification tools applicable for mainstream software development. To help the developers of KeY, its users, and the deductive verification community, we summarize our experiences with KeY 2.6.1 in specifying and verifying real-world Java code from a users perspective. To this end, we concentrate on parts of the Collection-API of OpenJDK, where an informal specification exists. While we describe how we bridged informal and formal specification, we also exhibit accompanied challenges that we encountered. Our experiences are that (a) in principle, deductive verification for API-like code bases is feasible, but requires high expertise, (b) developing formal specifications for existing code bases is still notoriously hard, and (c) the under-specification of certain language constructs in Java is challenging for tool builders.
  • Alexander Knüppel, Thomas Thüm, Carsten Pardylla, and Ina Schaefer. Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY. In International Conference on Interactive Theorem Proving (ITP), July 2018. To appear.
    As formal verification of software systems is a complex task comprising many algorithms and heuristics, modern theorem provers offer numerous parameters that are to be selected by a user to control how a piece of software is verified. Evidently, the number of parameters even increases with each new release. One challenge is that default parameters are often insufficient to close proofs automatically and are not optimal in terms of verification effort. The verification phase becomes hardly accessible for non-experts, who typically must follow a time-consuming trial-and-error strategy to choose the right parameters for even trivial pieces of software. To aid users of deductive verification, we apply machine learning techniques to empirically investigate which parameters and combinations thereof impair or improve provability and verification effort. We exemplify our procedure on the deductive verification system KeY 2.6.1 and formulate 38 hypotheses of which only three have been invalidated. We identified parameters that represent a trade-off between high provability and low verification effort, enabling the possibility to prioritize the selection of a parameter for either direction. Our insights give tool builders a better understanding of their control parameters and constitute a stepping stone towards automated deductive verification and better applicability of verification tools for non-experts.
  • Alexander Knüppel, Thomas Thüm, Stephan Mennicke, Jens Meinicke, and Ina Schaefer. Is There a Mismatch Between Real-World Feature Models and Product-Line Research?. In Software Engineering, Bonn, Germany, March 2018. Gesellschaft für Informatik (GI).
    This work has been presented at the joint meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering in Paderborn, Germany. Feature modeling has emerged as the de-facto standard to capture variability of a software product line in a compact and understandable fashion. Multiple feature modeling languages that evolved over the last decades to manage industrial-size product lines have been proposed. However, less expressive languages, solely permitting require and exclude constraints, are permanently and carelessly used in product-line research. We address the problem whether those less expressive languages are sufficient for industrial product lines. We developed an algorithm to eliminate complex cross-tree constraints in a feature model, enabling the combined usage of tools and algorithms working with different feature model dialects in a plug-and-play manner. However, the scope of our algorithm is limited. Our evaluation on large feature models, including the Linux kernel, gives evidence that require and exclude constraints are not sufficient to express real-world feature models. Hence, we promote that research on feature models needs to consider arbitrary propositional formulas as cross-tree constraints prospectively.

2017

  • Alexander Knüppel, Thomas Thüm, Stephan Mennicke, Jens Meinicke, and Ina Schaefer. Is There a Mismatch Between Real-World Feature Models and Product-Line Research?. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE). 2017. To appear. Software artifacts available: GitHub
    Feature modeling has emerged as the de-facto standard to compactly capture the variability of a software product line. Multiple feature modeling languages have been proposed that evolved over the last decades to manage industrial-size product lines. However, less expressive languages, solely permitting require and exclude constraints, are permanently and carelessly used in product-line research. We address the problem whether those less expressive languages are sufficient for industrial product lines. We developed an algorithm to eliminate complex cross-tree constraints in a feature model, enabling the combination of tools and algorithms working with different feature model dialects in a plug-and-play manner. However, the scope of our algorithm is limited. Our evaluation on large feature models, including the Linux kernel, gives evidence that require and exclude constraints are not sufficient to express real-world feature models. Hence, we promote that research on feature models needs to consider arbitrary propositional formulas as cross-tree constraints prospectively.

2016


  aktualisiert am 02.09.2016
TU_Icon_E_Mail_1_17x17_RGB Zum Seitenanfang