Navigation

Björn Wachter

About Me

I have moved to the University of Oxford. My new website there is:
http://www.comlab.ox.ac.uk/people/bjoern.wachter/

I began my studies of CS at the Universität des Saarlandes in winter 2000. In 2005, I finished my Master's thesis and joined the lab to pursue a PhD. I have defended my dissertation in December 2010.

Research Interests

Abstraction Refinement
Abstract Interpretation
Model Checking
Quantitative models (probabilistic, stochastic, timed)
Timing Analysis - Worst-case execution time

PASS

Check out PASS a tool that does abstraction refinement for infinite-state probabilistic models.

Projects

I contributed to the AVACS - Automatic Verification and Analysis of Complex Systems Project.

Publications

Journal Papers

Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains
E. M. Hahn, H. Hermanns, B. Wachter, and L. Zhang
Fundamenta Informaticae, 95, 2009. [url] [bib]

@ARTICLE{Hahn09a,
   author = {E. Moritz Hahn and Holger Hermanns and Bj\"orn Wachter and Lijun Zhang},
   title = {Time-Bounded Model Checking of Infinite-State Continuous-Time {Markov} Chains},
   journal = {Fundamenta Informaticae},
   year = {2009},
   volume = {95},
   pages = {129--155},
   url = {http://dx.doi.org/10.3233/FI-2009-145}
 }

Conference Papers

Best Probabilistic Transformers
B. Wachter, and L. Zhang
VMCAI, 2010. [pdf] [bib]

@INPROCEEDINGS{Wachter10,
   author = {Bj\"orn Wachter and Lijun Zhang},
   title = {Best Probabilistic Transformers},
   booktitle = {VMCAI},
   year = {2010},
   pages = {362--379},
   publisher = {Springer Verlag},
   url = {http://rw4.cs.uni-saarland.de/~bwachter/papers/vmcai10-ai-mdp.pdf}
 }

Static Timing Analysis for Hard Real-Time Systems
R. Wilhelm, S. Altmeyer, C. Burguière, D. Grund, J. Herter, J. Reineke, B. Wachter, and S. Wilhelm
VMCAI, 2010. [doi] [bib]

@INPROCEEDINGS{Wilhelm10,
   author = {Reinhard Wilhelm and Sebastian Altmeyer and Claire Burgui\`ere and Daniel Grund and J\"org Herter and Jan Reineke and Bj\"orn Wachter and Stephan Wilhelm},
   title = {Static Timing Analysis for Hard Real-Time Systems},
   booktitle = {VMCAI},
   year = {2010},
   pages = {3--22},
   publisher = {Springer Verlag},
   doi = {10.1007/978-3-642-11319-2_3}
 }

INFAMY: An Infinite-State Markov Model Checker
E. M. Hahn, H. Hermanns, B. Wachter, and L. Zhang
Computer Aided Verification, 2009. [doi] [bib]

@INPROCEEDINGS{Hahn09,
   author = {Ernst Moritz Hahn and Holger Hermanns and Bj\"orn Wachter and Lijun Zhang},
   title = {{INFAMY}: An Infinite-State Markov Model Checker},
   booktitle = {Computer Aided Verification},
   year = {2009},
   editor = {Ahmed Bouajjani and Oded Maler},
   volume = {5643},
   series = {LNCS},
   pages = {641--647},
   publisher = {Springer},
   doi = {10.1007/978-3-642-02658-4_49}
 }

Improving Timing Analysis for Matlab Simulink/Stateflow
L. Tan, B. Wachter, P. Lucas, and R. Wilhelm
Proceedings of the 2nd International Workshop on Model Based Architecting and Construction of Embedded Systems (ACES-MB), 2009. [pdf] [bib]

@INPROCEEDINGS{Tan09a,
   author = {Lili Tan and Bj\"orn Wachter and Philipp Lucas and Reinhard Wilhelm},
   title = {Improving Timing Analysis for {Matlab} {Simulink}/{Stateflow}},
   booktitle = {Proceedings of the 2nd International Workshop on Model Based Architecting and Construction of Embedded Systems (ACES-MB)},
   year = {2009},
   editor = {Stefan Van Baelen and Thomas Weigert and Ileana Ober and Huascar Espinoza},
   pages = {59--63},
   url = {http://ceur-ws.org/Vol-507/paper05.pdf}
 }

Symbolic State Traversal for WCET Analysis
S. Wilhelm, and B. Wachter
International Conference on Embedded Software, 2009. [bib]

@INPROCEEDINGS{Wilhelm09a,
   author = {Stephan Wilhelm and Bj\"orn Wachter},
   title = {Symbolic State Traversal for {WCET} Analysis},
   booktitle = {International Conference on Embedded Software},
   year = {2009},
   pages = {137--146},
   month = {October},
 }

Probabilistic CEGAR
H. Hermanns, B. Wachter, and L. Zhang
CAV, 2008. [pdf] [bib]

@INPROCEEDINGS{Hermanns08,
   author = {Holger Hermanns and Bj\"orn Wachter and Lijun Zhang},
   title = {Probabilistic {CEGAR}},
   booktitle = {CAV},
   year = {2008},
   editor = {Aarti Gupta and Sharad Malik},
   volume = {5123},
   series = {LNCS},
   pages = {162--175},
   publisher = {Springer Verlag},
   note = {Princeton, NJ, USA},
   url = {http://rw4.cs.uni-saarland.de/~bwachter/papers/cav08-pcegar.pdf}
 }

Abstract Interpretation with Applications to Timing Validation
R. Wilhelm, and B. Wachter
CAV, 2008. [pdf] [bib]

@INPROCEEDINGS{Wilhelm08a,
   author = {Reinhard Wilhelm and Bj\"orn Wachter},
   title = {Abstract Interpretation with Applications to Timing Validation},
   booktitle = {CAV},
   year = {2008},
   editor = {Aarti Gupta and Sharad Malik},
   volume = {5123},
   series = {LNCS},
   pages = {22--36},
   publisher = {Springer Verlag},
   note = {Princeton, NJ, USA},
   url = {http://rw4.cs.uni-saarland.de/~bwachter/papers/cav08-ai-tutorial.pdf}
 }

Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains
L. Zhang, H. Hermanns, E. M. Hahn, and B. Wachter
ACSD, 2008. [pdf] [bib]

@INPROCEEDINGS{Zhang08,
   author = {Lijun Zhang and Holger Hermanns and E. Moritz Hahn and Bj\"orn Wachter},
   title = {Time-Bounded Model Checking of Infinite-State Continuous-Time Markov Chains},
   booktitle = {ACSD},
   year = {2008},
   note = {Xi'an, China},
   url = {http://rw4.cs.uni-saarland.de/~bwachter/papers/acsd08-time-bounded.pdf}
 }

The Spotlight Principle: On Process-Summarizing State Abstractions
B. Wachter, and B. Westphal
Verification, Model Checking and Abstract Interpretation, 2007. [bib]

@INPROCEEDINGS{Wachter07,
   author = {Bj\"orn Wachter and Bernd Westphal},
   title = {The Spotlight Principle: On Process-Summarizing State Abstractions},
   booktitle = {Verification, Model Checking and Abstract Interpretation},
   year = {2007},
   editor = {Andreas Podelski and Byron Cook},
   volume = {4349},
   series = {LNCS},
   publisher = {Springer Verlag},
   note = {Nice, France},
 }

Probabilistic Model Checking Modulo Theories
B. Wachter, L. Zhang, and H. Hermanns
Proceedings of the Fourth International Conference on the Quantitative Evaluation of Systems, 2007. [bib]

@INPROCEEDINGS{Wachter07a,
   author = {Bj\"orn Wachter and Lijun Zhang and Holger Hermanns},
   title = {Probabilistic Model Checking Modulo Theories},
   booktitle = {Proceedings of the Fourth International Conference on the Quantitative Evaluation of Systems},
   year = {2007},
   month = {September},
 }

Towards Symbolic State Traversal for Efficient WCET Analysis of Abstract Pipeline and Cache Models
S. Wilhelm, and B. Wachter
Proceedings of Seventh International Workshop on Worst-Case Execution Time Analysis, 2007. [pdf] [bib]

@INPROCEEDINGS{Wilhelm07a,
   author = {Stephan Wilhelm and Bj\"orn Wachter},
   title = {Towards Symbolic State Traversal for Efficient {WCET} Analysis of Abstract Pipeline and Cache Models},
   booktitle = {Proceedings of Seventh International Workshop on Worst-Case Execution Time Analysis},
   year = {2007},
   month = {July},
   url = {http://www.irit.fr/wcet2007/finalpapers/wilhelm.pdf}
 }

A Definition and Classification of Timing Anomalies
J. Reineke, B. Wachter, S. Thesing, R. Wilhelm, I. Polian, J. Eisinger, and B. Becker
Proceedings of 6th International Workshop on Worst-Case Execution Time (WCET) Analysis, 2006. [pdf] [slides] [bib]

@INPROCEEDINGS{Reineke06b,
   author = {Jan Reineke and Bj\"orn Wachter and Stephan Thesing and Reinhard Wilhelm and Ilia Polian and Jochen Eisinger and Bernd Becker},
   title = {A Definition and Classification of Timing Anomalies},
   booktitle = {Proceedings of 6th International Workshop on Worst-Case Execution Time ({WCET}) Analysis},
   year = {2006},
   month = {July},
   slides = {http://rw4.cs.uni-saarland.de/~reineke/talks/timingAnomaliesWCET06.ppt},
   url = {http://rw4.cs.uni-saarland.de/~reineke/publications/TimingAnomaliesWCET06.pdf}
 }

Explaining Data Type Reduction in the Shape Analysis Framework
B. Wachter
Workshop Trustworthy Software 2006, 2006. [bib]

@INPROCEEDINGS{Wachter06,
   author = {Bj\"orn Wachter},
   title = {Explaining Data Type Reduction in the Shape Analysis Framework},
   booktitle = {Workshop Trustworthy Software 2006},
   year = {2006},
   editor = {Serge Autexier and Stephan Merz and Leon van der Torre and Reinhard Wilhelm and Pierre Wolper},
   publisher = {Internationales Begegnungs- und Forschungszentrum f\"ur Informatik (IBFI), Schloss Dagstuhl, Germany},
   optaddress = {Dagstuhl, Germany}
 }

MSc Theses

Checking Universally Quantified Temporal Properties with Three-Valued Analysis
B. Wachter
Universität des Saarlandes, 2005. [bib]

@MASTERSTHESIS{Wachter05,
   author = {Bj\"orn Wachter},
   title = {Checking Universally Quantified Temporal Properties with Three-Valued Analysis},
   school = {Universit\"at des Saarlandes},
   year = {2005},
 }

Technical Reports

Best Probabilistic Transformers and Beyond
B. Wachter, and L. Zhang
Technical Report, SFB/TR 14 AVACS, 2009. [pdf] [bib]

@TECHREPORT{Wachter09,
   author = {Bj\"orn Wachter and Lijun Zhang},
   title = {Best Probabilistic Transformers and Beyond},
   institution = {SFB/TR 14 AVACS},
   year = {2009},
   type = {Reports of SFB/TR 14 AVACS},
   number = {48},
   month = {April},
   note = {ISSN: 1860-9821, http://www.avacs.org.},
   editor = {Bernd Becker and Werner Damm and Martin Fr\"anzle and Ernst-R\"udiger Olderog and Andreas Podelski and Reinhard Wilhelm},
   series = {ATR},
   subproject = {S2},
   url = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_048.pdf}
 }

On Probabilistic CEGAR
H. Hermanns, B. Wachter, and L. Zhang
Technical Report, SFB/TR 14 AVACS, 2007. [pdf] [bib]

@TECHREPORT{Hermanns07,
   author = {Holger Hermanns and Bj\"orn Wachter and Lijun Zhang},
   title = {On Probabilistic {CEGAR}},
   institution = {SFB/TR 14 AVACS},
   year = {2007},
   type = {Reports of SFB/TR 14 AVACS},
   number = {33},
   month = {December},
   editor = {Bernd Becker and Werner Damm and Martin Fr\"anzle andErnst-R\"udiger Olderog and Andreas Podelski and Reinhard Wilhelm},
   series = {ATR},
   subproject = {S2},
   url = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_033.pdf}
 }

Teaching

TA: Modular Static Analysis, 2007
TA: Compiler Construction, 2006

Address

Björn Wachter
Chair for Programming Languages and Compiler Construction
FR. 6.2 - Informatik
Universität des Saarlandes
Postfach 15 11 50
D-66041 Saarbrücken

Building E1 3, Room 431
Tel: +49 (681) 302 3915
Fax: +49 (681) 302 3065
Mail: bwachter(at)cs(dot)uni-saarland(dot)de

Compiler Design Lab