Home Publications Tools Links Pictures


Björn Wachter

Universität des Saarlandes, Building E1 3, Room 431
Im Stadtwald - Gebäude E1 3
Postfach 15 11 50
66041 Saarbrücken, Germany
@: bwachter(at)cs(dot)uni-sb(dot)de , phone: +49-681-302-3915


Formal methods, abstraction, analysis of probabilistic systems

Probabilistic models are widely used to analyze embedded, networked, and more recently biological systems. The goal of my research is to develop analysis techniques for large or even infinite-state probabilistic models. To this end, concise abstractions are crucial: abstractions that are precise enough to obtain the desired information and yet small enough to be effeciently analyzable. We develop novel abstraction refinement techniques for probabilistic systems to find concise abstractions.

This is joint work with Lijun Zhang and Holger Hermanns in the context of AVACS.
Best Probabilistic Transformers (VMCAI'10)
Symbolic State Traversal for WCET Analysis (EMSOFT'09)
Tutorial: Abstract Interpretation with Applications to Timing Validation (CAV'08)
Probabilistic CEGAR (CAV'08)
Time-Bounded Model Checking of Infinite-State CTMCs (ACSD'08)  
Probabilistic Model Checking Modulo Theories (QEST'07)  
The Spotlight Principle (VMCAI'07)  

* The documents referenced are included by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright.

Chair for Programming Languages and Compiler Construction