Alexander Weigl

Dr. rer. nat. Alexander Weigl
Executive Manager of HGF Pilot Program Core Informatics
Post-Doctoral Researcher

weigl@kit.edu

Building 50.34; Room 15?
Am Fasanengarten 5
DE-76131 Karlsruhe
Germany

Phone: +49 721 608 44324
Fax: +49 721 608 44021

S/MIME Cert
GPG: 9C63 C6FC 02D8 6A0E 6326 4B25 8864 9644 84D2 2F29
@tk5165:kit.edu
0000-0001-8446-4598
wadoon
wadoon
Goolge Scholar
DBLP
Activities · Projects · Teaching · Software · Publications

Projects

KiKIT

In the information age, computers are a key driver in all areas of research, technology, business, and society. Therefore, high-quality software, hardware, and AI models are necessary to maintain digital sovereignty and need provisional research. Currently, research on core informatics, i.e. research on fundamental methods of informatics that can be applied in various applications and domains, is a blind spot in the Helmholtz Association, which has informatics research but mainly weaved into their specific classical research area.

Through the Pilot Program Kerninformatik am KIT (KiKIT), the research on core informatics is to become a focus of Helmholtz research. KiKIT focuses on the research of novel general methods in the fields of algorithm and software engineering, data analysis, and machine learning as well as hardware and network systems. Moreover, KiKIT pursues the goal of providing stable research tools (research software, AI models, etc.) to accelerate other research activities within Helmholtz as well as to support innovation in industry.

Currently, there are 26 PIs, and 40 researchers in 36 projects working on topics like Sustainability, Correctness, Explainability, and Performance of Software and Hardware following the goal of strengthening Germany’s sovereignty in informatics.

KiKITs Homepage

SofDCar

All project partners of the SofDCar Alliance are focussing their research on the challenges of future E/E & SW architecture in vehicles.

Each vehicle is seen as one piece in a network of all vehicles and the infrastructure. Its integration will be enabled via “data loops” and new-type “digital twins”, thereby paving the path to digital sustainability (of today’s and tomorrow’s vehicle generations) and enabling efficient data structures and innovative use cases throughout the whole vehicle lifetime (Re-Deployment).

This project is part of a government-sponsored research program. It is sponsored by the German Ministry of Business Affairs and Climate Control (BMWK).

Project Homepage

CHANGE APS

KeY

The KeY System is a formal software development tool that aims to integrate design, implementation, formal specification, and formal verification of object-oriented software as seamlessly as possible. At the core of the system is a novel theorem prover for the first-order Dynamic Logic for Java with a user-friendly graphical interface. The project was started in November 1998 at the University of Karlsruhe. It is now a joint project of KIT, Chalmers University of Technology, Gothenburg, and TU Darmstadt. The KeY tool is available for download.

KASTEL

The main topics intelligent infrastructure, cloud computing and public security challenge the IT security of the future. In addition to the classical term of security one has to deal with threats from the inside as well. It is not enough anymore only to look at security issues of system components. We have to focus on transdisciplinary methods. The Kompetenzzentrum für Angewandte Sicherheits-TEchnoLogie (KASTEL) is a research center for cyber security and combine several areas of IT security and their users.

IMPROVE APS

The vision for this project is to advance technology such that regression verification methods are available that will be routinely used for ensuring correctness in the evolution processes for long-living reliable systems requiring frequent re-validation. The goal of regression verification is to formally prove that software remains correct through its evolution, changes have the desired effect, and no new bugs are introduced. Regression verification avoids the main bottleneck for the routine practical use of formal verification, namely the need to write full functional specifications (which is a huge effort). Also, given two program versions or variants that are both complex but similar to each other, the effort for verifying the relation between them mainly depends on the difference between the programs and not on their overall size and complexity.

DeduSec: Program-level Specification and Deductive Verification of Security Properties

Reliably Secure Software Systems – RS³ In recent years tremendous progress has been achieved in formal verification of functional properties of computer programs. At the same time seminal papers have been published showing that it is in principle possible to formulate information-flow problems as proof obligations in program logics. The overall goal of the project is to leverage these advances together with our own experience in formal methods for functional properties in order to specify and verify security properties. DeduSec Project

Software

CAgen — Full Refinement Approach for Design-by-Contract of Reactive System in C

cagen is a prototypical helper for the work with contract automata.

This program offers you the construction of proof obligations based on a system description and contract automata. There are different proof obligations.

We recommend you to use nuXmv, cbmc and seahorn.

cagen at github Gecko is a graphical modelling tool for contract automata

VerifAPS — Library for the Verification of Automated Producton System Software

VerifAPS (Verifiaction for Automated Producton System) is a library for supporting the verification of software for automation manufacturing domain.

Allows the parsing and analyzation of Structured Text, Sequential Function Chart, Instruction List and Function Block Diagrams. Ladder Diagrams are incoming. This also includes reading from PCLOpenXML and Object-oriented extension (IEC 61131 2013). The library offers symbolic execution expressible in SMV or SMT files. Controller for nuXmv/nuSMV is including, e.g., parsing of counter example.

Website Github

Upon VerifAPS lives geteta and stvs, which offers functionalities for *Generalized Test Tables

Generalised test tables extend the concept of test tables, which are already frequently used in quality management of reactive systems. The main idea is to allow more general table entries, thus enabling a table to capture not just a single test case but a family of similar behavioural cases. We show how generalised test tables can be encoded into verification conditions for state-of-the-art model checkers. — from the paper

stvs provides a graphical user interface for the verification of Structured Text source code against generalized test tables. It is a graphical frontend for the geteta backend, providing a useful and beautiful user interface, e.g., a visualization of specification violations. stvs is open source, provided under GNU Public License v3.

Features includes

The Backend geteta ∣ The Frontend stvs

jmltoolkit

Parser and Tools for the processing of the Java Modeling Language

The KeY theorem prover

#PI — Quantified Information Flow of C programs

sharpPI is a tool for quantified information flow analysis with support Shannon Entropy based on the SAT-based approach of Vladimir Klebanov.

QIF with sharpPI has following features:

Website

ApproxMC-p(y)

ApproxMC-p is a (δ, ϵ)-counter for models of propositional formulas with support for projection. In short, ApproxMC-p calculates an model count M for an propositional formula φ with projection on Δ, s.t. the confidence δ and the tolerance ϵ is maintained.

Website

Smaller Tools

Teaching

WS 2015/16: Proseminar Desasters in der Software-Sicherheit Topics are:

Buffer Overflow
Storing Passwords

SS 2015:Proseminar Desasters in der Software-Sicherheit Topics are:

Therac-25 Desaster
Smartcard Vunerability

Open Theses

Publications

2021

2020

2019

2018

2017

2016

2015

2012