Alexander Weigl

Dr. rer. nat. Alexander Sebastian Weigl, M. Sc.

Executive Manager of HGF Pilot Program Core Informatics

Post-Doctoral Researcher

Fingerpint: 9C63 C6FC 02D8 6A0E 6326 4B25 8864 9644 84D2 2F29
GPG-Key
S/MIME of KIT-CA

KIT / Institute for Theoretical Computer Science
Am Fasanengarten 5
76131 Karlsruhe
Germany

Building 50.34 Office 225
(Tel) +49 721 608 44324
(Fax) +49 721 608 44021
weigl1968962344Xfd4∂kit.edu
Matrix: @tk5165:kit.edu

Activities · Projects · Teaching · Software · Publications

Activities

2021
  • Finish my PhD studies with the degree Dr. rer. nat.
  • Teaching Assistant for Formale Systeme
  • Papers on: NFM'2021, QEST'2021, DPM'2021
  • Organising the VerifyThis LongTerm Challenges
2020
  • Teaching Assistant for Formale Systeme
  • Attending Formalise'2020 in Seoul
  • Organising the VerifyThis LongTerm Challenges
2019
2018
2017
  • Attending iFM 2017
  • Attending INDIN 2017 with two papers
  • Attending NATO Summer School in Markoberdorf, Bavaria, Germany
2016
2015

Projects

Core-Informatics


CHANGE APS


SofDCar


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

KASTEL logo 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.

Finished Projects

IMPROVE APS

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. IMPROVE-APS Project


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

xorblast

A CNF preprocessor for xor constraints with support of Gauss-Jordan elimination.

#PI

... soon ...

ReVeForPLC

iec61131lang Parser and AST for languages of the IEC61131 norm.


Medical Simuation Markup Language (MSML)

msml at Github.
The medical simulation markup language (MSML) is a flexible XML-based description for the biomechanical modeling workflow and finite-element based biomechanical models. MSML helps you to create biomechanical models from tomographic data, export them to FE solvers and analyze the results. It is very flexible as already existing components (e.g. segmentation algorithms, meshers) can usually be integrated into the framework by providing a single additional XML-file. MSML was created in the SFB125 in a coorperation between KIT and DKFZ.

Publications

2024
Title Author(s) Source
The Java Verification Tool KeY: A TutorialBernhard Beckert
Richard Bubel
Daniel Drodt
Reiner Hähnle
Florian Lanzinger
Wolfram Pfeifer
Mattias Ulbrich
Alexander Weigl
26th International Symposium on Formal Methods (FM 2024)
Quantifying Software Correctness by Combining Architecture Modeling and Formal Program AnalysisFlorian Lanzinger
Christian Martin
Frederik Reiche
Samuel Teuber
Robert Heinrich
Alexander Weigl
Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing, SAC 2024
2023
Title Author(s) Source
A SAT-Benchmark Set from the Approximation of Trigonometric Functions for SAT-based VerificationKai Hiller
Alexander Weigl
Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions
Formal Specification and Verification of JDK's Identity Hash Map ImplementationMartin de Boer
Stijn de Gouw
Jonas Klamroth
Christian Jung
Mattias Ulbrich
Alexander Weigl
Formal Aspects Comput. 35(3)
2022
Title Author(s) Source
A Refactoring for Data Minimisation Using Formal VerificationFlorian Lanzinger
Mattias Ulbrich
Alexander Weigl
11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering (ISoLA 2022)
Formal Specification and Verification of JDK’s Identity Hash Map ImplementationMartin de Boer
Stijn de Gouw
Jonas Klamroth
Christian Jung
Mattias Ulbrich
Alexander Weigl
17th International Conference on integrated Formal Methods (iFM 2022)
Formal Specification and Verification of JDK’s Identity Hash Map Implementation (Long Version)Martin de Boer
Stijn de Gouw
Jonas Klamroth
Christian Jung
Mattias Ulbrich
Alexander Weigl
Karlsruhe Institute of Technology (KIT) 1000145727
The counterSharp Model Counting BenchmarkSamuel Teuber
Alexander Weigl
Karlsruhe Institute of Technology 2022-02
Towards a Formal Approach for Data Minimization in ProgramsFlorian Lanzinger
Alexander Weigl
Data Privacy Management, Cryptocurrencies and Blockchain Technology
Generalized Test Tables: A Domain-Specific Specification Language for Automated Production SystemsBernhard Beckert
Mattias Ulbrich
Birgit Vogel‑Heuser
Alexander Weigl
Theoretical Aspects of Computing - ICTAC 2022
2021
Title Author(s) Source
Upper Bound Computation of Information Leakages for Unbounded RecursionJohannes Bechberger
Alexander Weigl
19th International Conference on Software Engineering and Formal Methods (SEFM 2021)
Formal Specification and Verification for Automated Production SystemsAlexander Sebastian WeiglKarlsruhe Institute of Technology (KIT) (December 2021)
Scalability and Precision by Combining Expressive Type Systems and Deductive VerificationFlorian Lanzinger
Alexander Weigl
Mattias Ulbrich
Werner Dietl
Proceedings of the ACM on programming languages 5(OOPSLA)
Quantifying Software Reliability via Model-CountingSamuel Teuber
Alexander Weigl
18th International Conference on Quantitative Evaluation of Systems (QEST 2021)
Runtime Verification of Generalized Test TablesAlexander Weigl
Mattias Ulbrich
Shmuel S. Tyszberowicz
Jonas Klamroth
NASA Formal Methods - 13th International Symposium, NFM 2021, Virtual Event, May 24-28, 2021, Proceedings
Table-based formal specification approaches for control engineers—empirical studies of usabilitySuhyun Cha
Birgit Vogel‑Heuser
Alexander Weigl
Mattias Ulbrich
Bernhard Beckert
IET Cyber-Physical Systems: Theory and Applications
2020
Title Author(s) Source
The VerifyThis Collaborative Long Term ChallengeMarieke Huisman
Raúl Monti
Mattias Ulbrich
Alexander Weigl
Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY, Part IV: Feasibility and Usability
Modular Regression Verification for Reactive SystemsAlexander Weigl
Mattias Ulbrich
Daniel Lentzsch
9th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2020), Part II: Engineering Principles
VerifyThis Long-term Challenge 2020: Proceedings of the Online-EventMarieke Huisman
Raúl E. Monti
Mattias Ulbrich
Alexander Weigl
Institut für Theoretische Informatik (ITI), KIT 2020
Relational Test Tables: A Practical Specification Language for Evolution and SecurityAlexander Weigl
Mattias Ulbrich
Suhyun Cha
Bernhard Beckert
Birgit Vogel‑Heuser
FormaliSE@ICSE 2020: 8th International Conference on Formal Methods in Software Engineering, Seoul, Republic of Korea, July 13, 2020
On the Preservation of the Trust by Regression Verification of PLC software for Cyber-Physical Systems of SystemsSuhyun Cha
Mattias Ulbrich
Alexander Weigl
Bernhard Beckert
Kathrin Land
Birgit Vogel‑Heuser
17th IEEE International Conference on Industrial Informatics (INDIN 2019)
2019
Title Author(s) Source
KASTEL Industry 4.0 Demonstrator: Provably Forgetting Information in PLC softwareAlexander WeiglPresentation in the KASTEL Seminar, Karlsruhe, Germany, October 10
Formal Verification of Evolutionary ChangesBernhard Beckert
Jakob Mund
Mattias Ulbrich
Alexander Weigl
Managed Software Evolution
2018
Title Author(s) Source
Applicability of Generalized Test Tables: A Case Study Using the Manufacturing System Demonstrator xPPUSuhyun Cha
Alexander Weigl
Mattias Ulbrich
Bernhard Beckert
Birgit Vogel‑Heuser
Automatisierungstechnik Special Issue
Achieving delta description for the system software of an automated production evolution based on partially inferenced modelSuhyun Cha
Alexander Weigl
Mattias Ulbrich
Bernhard Beckert
Birgit Vogel‑Heuser
14th IEEE International Conference on Automation Science and Engineering (CASE 2018)
Adding Text-Based Interaction to a Direct-Manipulation Interface for Program Verification – Lessons LearnedSarah Grebing
An Thuy Tien Luong
Alexander Weigl
13th International Workshop on User Interfaces for Theorem Provers (UITP 2018)
Relational Equivalence Proofs Between Imperative and MapReduce AlgorithmsBernhard Beckert
Timo Bingmann
Moritz Kiefer
Peter Sanders
Mattias Ulbrich
Alexander Weigl
10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018)
Proving Equivalence Between Imperative and MapReduce Implementations Using Program TransformationsBernhard Beckert
Timo Bingmann
Moritz Kiefer
Peter Sanders
Mattias Ulbrich
Alexander Weigl
Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation (MARS/VPT@ETAPS 2018)
Debugging Program Verification Proof Scripts (Tool Paper)Bernhard Beckert
Sarah Grebing
Alexander Weigl
CoRR abs/1804.04402
Applicability of Generalized Test Tables: A Case Study Using the Manufacturing System Demonstrator xPPUSuhyun Cha
Alexander Weigl
Mattias Ulbrich
Bernhard Beckert
Birgit Vogel‑Heuser
Automatisierungstechnik 66(10)
2017
Title Author(s) Source
Generalised Test Tables: A Practical Specification Language for Reactive SystemsBernhard Beckert
Suhyun Cha
Mattias Ulbrich
Birgit Vogel‑Heuser
Alexander Weigl
13th International Conference on integrated Formal Methods (iFM 2017)
Generation of Monitoring Functions in Production Automation Using Test SpecificationsSuhyun Cha
Sebastian Ulewicz
Birgit Vogel‑Heuser
Alexander Weigl
Mattias Ulbrich
Bernhard Beckert
15th IEEE International Conference on Industrial Informatics (INDIN 2017)
Generalized Test Tables: A Powerful and Intuitive Specification Language for Reactive SystemsAlexander Weigl
Franziska Wiebe
Mattias Ulbrich
Sebastian Ulewicz
Suhyun Cha
Michael Kirsten
Bernhard Beckert
Birgit Vogel‑Heuser
15th IEEE International Conference on Industrial Informatics (INDIN 2017)
2016
Title Author(s) Source
Sound Probabilistic #SAT with ProjectionVladimir Klebanov
Alexander Weigl
Jörg Weisbarth
14th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2016)
Efficient SAT-based Pre-image Enumeration for Quantitative Information Flow in ProgramsAlexander Weigl5th International Workshop on Quantitative Aspects of Security Assurance (QASA 2016)
A Verification-Supported Evolution Approach to Assist Software Application Engineers in Industrial Factory AutomationSebastian Ulewicz
Mattias Ulbrich
Alexander Weigl
Michael Kirsten
Franziska Wiebe
Bernhard Beckert
Birgit Vogel‑Heuser
IEEE International Symposium on Assembly and Manufacturing (ISAM 2016)
2015
Title Author(s) Source
Regression Verification for Programmable Logic Controller SoftwareBernhard Beckert
Mattias Ulbrich
Birgit Vogel‑Heuser
Alexander Weigl
17th International Conference on Formal Engineering Methods (ICFEM 2015)
Proving Equivalence between Control Software Variants for Programmable Logic Controllers - Using Regression Verification to Reduce Unneeded Variant DiversitySebastian Ulewicz
Mattias Ulbrich
Alexander Weigl
Bernhard Beckert
Birgit Vogel‑Heuser
20th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2015)
Regression Verification for Programmable Logic Controller SoftwareBernhard Beckert
Mattias Ulbrich
Birgit Vogel‑Heuser
Alexander Weigl
Karlsruhe Institute of Technology, Department of Informatics 2015-06
Regression Verification for Programmable Logic Controller SoftwareAlexander Sebastian WeiglKarlsruhe Institute of Technology (January 2015)

Teaching

SS 2020

WS 2019/20

SS 2019

WS 2018/19

SS 2018

WS 2017/18

SS 2017

WS 2016/17: Praxis der Software-Entwicklung

SS 2016: Proseminar Desasters in der Software-Sicherheit

Topics are:
  • Verifikation von med. Richtlinien
  • Probabilistisches Model-Checking

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