|
Alexander Sebastian Weigl, M. Sc. Researcher/PhD Student |
|
|
KIT /
Institute for Theoretical Computer Science
|
||
Activities
- 2016
-
- I am going to hold presentation about #PI at QASA'16
- Attendance SAT/SMT/AR Summer School 2015
- Published
Sound Probabilistic #SAT with Projection at QAPL'16
- 2015
-
- Attendance to VTSA 2015
Projects
DeduSec: Program-level Specification and Deductive Verification of Security Properties
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
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
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
| Title | Author(s) | Source |
|---|---|---|
| Formal Verification of Evolutionary Changes | Bernhard Beckert Jakob Mund Mattias Ulbrich Alexander Weigl | Managed Software Evolution |
| Title | Author(s) | Source |
|---|---|---|
| Generalised Test Tables: A Practical Specification Language for Reactive Systems | Bernhard 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 Specifications | Suhyun 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 Systems | Alexander 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) |
| Title | Author(s) | Source |
|---|---|---|
| Sound Probabilistic #SAT with Projection | Vladimir 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 Programs | Alexander Weigl | 5th International Workshop on Quantitative Aspects of Security Assurance (QASA 2016) |
| A Verification-Supported Evolution Approach to Assist Software Application Engineers in Industrial Factory Automation | Sebastian Ulewicz Mattias Ulbrich Alexander Weigl Michael Kirsten Franziska Wiebe Bernhard Beckert Birgit Vogel‑Heuser | IEEE International Symposium on Assembly and Manufacturing (ISAM 2016) |
| Title | Author(s) | Source |
|---|---|---|
| Regression Verification for Programmable Logic Controller Software | Bernhard 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 Diversity | Sebastian 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 Software | Bernhard Beckert Mattias Ulbrich Birgit Vogel‑Heuser Alexander Weigl | Karlsruhe Institute of Technology, Department of Informatics 2015-06 |
| Regression Verification for Programmable Logic Controller Software | Alexander Sebastian Weigl | Karlsruhe Institute of Technology (January 2015) |
Teaching
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
