Alexander Weigl

Alexander Sebastian Weigl, M. Sc.

Researcher/PhD Student

Fingerpint: 9C63 C6FC 02D8 6A0E 6326 4B25 8864 9644 84D2 2F29
GPG-Key

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
weigl2103500544Xfd4∂kit.edu

Activities

2016
2015

Projects

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


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

Software

VerifAPS — Verification for Automated Production System

There are several software modules (Maven projects) available:
  • iec61131lang Parser and AST for languages of the IEC61131 norm.
  • iec61131lang Symbolic Execution and Code Transformation for Sequential Function Charts and Structured Text.
  • iec-xml Support of PCLOpenXML.
  • smv-model AST and Generation of SMV modules.
  • geteta (GITHUB) Verification Engine for Generalized Test Tables

#PI — QIF analysis for C

#PI is a tool for analysis of Quantified Information Flow for C programs.

xorblast

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


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

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 2017: Praxis der Software-Entwicklung

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