-
Contact Information
Dr. Ralf Wimmer
Chair of Computer Architecture
Faculty of Engineering
Albert-Ludwigs-University Freiburg
Georges-Köhler-Allee, Building 51, Room 01..033
79110 Freiburg im Breisgau
GermanyPhone +49 761 203 8179
Fax +49 761 203 8142
E-Mail: wimmer AT informatik.uni-freiburg.de
-
Biography
- 1999-2004: Studies in Computer Science (major subject) and Microsystems Engineering (minor subject) at the Albert-Ludwigs-University Freiburg, Germany. During this time various jobs at the Institute of Computer Science, e. g. at the Chair of Computer Architecture, the Chair of Operating Systems, and the Institute for Applied Mathematics
- October 2005: VDI Award 2005, sponsored by VDI, the German Engineering Association, for the diploma thesis "Ganzzahlige lineare Optimierung und Separierung mit binären Entscheidungsdiagrammen" ("Integer linear optimization and separation with binary decision diagrams").
-
Since January 1st, 2005: PhD student at the
Chair of Computer Architecture
of Prof. Dr. Bernd Becker
- Since October 2006 (re-elected 2010): Member of the faculty council ("Fakultätsrat")
- October 2006 – September 2010: Member of the committee of study affairs ("Studienkommission") of the Faculty of Engineering at the University of Freiburg
- Spring/Summer 2010: Member of the review board for professorship applicants ("Berufungskommission") for "Algorithms and Complexity"
- From October 2010 on: Member of the examination board ("Prüfungsausschuss") of the Faculty of Engineering at the University of Freiburg
-
Teaching Activites:
- Sommercampus 2004: "Introduction to the Typesetting System LaTeX"
- Winter term 2004/2005: Assistant for the lecture "Technische Informatik"
- Summer term 2005: Assistant for the lecture "Technische Informatik II"
- Sommercampus 2005: "Introduction to the Typsetting System LaTeX".
- Winter term 2005/06: Assistant for the undergraduate seminar "Entwurfsmethoden" and of the graduate seminar "Advanced Model Checking"
- Summer term 2006: Assistant for the graduate lecture "Eingebettete Systeme II"
- Sommercampus 2006: "Introduction to the Typesetting System LaTeX"
- Winter term 2006/07: Assistant for the graduate seminar "Theoretical Foundations of Model checking"
- Summer term 2007: Assistant for the graduate seminar "Methoden der Verifikation"
- Winter term 2007/08: Assistant for the graduate seminar "SAT and beyond"
- Summer term 2008: Assistant for the lecture "Rechnerarchitektur"
- Winter term 2008/09: Assistant for the undergraduate seminar "Entwurfsmethoden" and for the graduate seminar "Satisfiability modulo theories (SMT)"
- Summer term 2009: Lecturer of the course "Einführung in die effiziente Softwareentwicklung"
- Winter term 2009/10: Assistant for the undergraduate seminar "Entwurfsmethoden" and lecturer of the graduate lecture "Eingebettete Systeme I"
- Summer term 2010: Assistant of the graduate seminar "Model Checking - Probabilistische und Echtzeitaspekte"
- Winter term 2010/11: Lecturer of the undergraduate lecture "Systeme I"
- Diploma thesis "Symbolische Berechnung von Bisimulationen" by Kelley Strampp
- Diploma thesis "Kompositionalität und Bounded Model Checking" by Natalia Kalinnik
- Student's project "xGen - ein Webportal zur Generierung von Übungsblättern" by Christoph Löffler
- Student's project "Ein semi-symbolischer Algorithmus für Paritätsspiele" by Georges Morbé
- Student's project "Probabilistisches Model-Checking mit exakter Arithmetik" by Alexander Kortus
- Bachelor thesis "Visualisierung von SAT-Algorithmen" by Markus Fuchs
- Diploma thesis "Bounded Model Checking für stochastische Systeme" by Alexander Kortus
- Diploma thesis "Model Checking für stochastische Systeme mit Black Boxes" by Eric Nyaben
- Bachelor Project "xGen2 - ein Portal zur Generierung von Übungsblättern" by Andreas Spilla, Daniel Frey, and Eduard Skaley.
- Bachelor Project "Implementierung eines stochastischen SAT-Solvers" by Jennifer Modes
- Diploma Thesis "Bounded Model Checking auf stochastischen Systemen" by Bettina Braitling (Continuation of Alexander Kortus' work)
- Bachelor Project "BDD-basierte Berechnung von Gegenbeispielen für Markow-Ketten" by Jan Hättig
-
Publications
Ganzzahlige lineare Optimierung und Separierung mit binären Entscheidungsdiagrammen (Diploma thesis, only available in German), November 2004 (pdf).
Bounded Model Checking and Inductive Verification of Hybrid Discrete-continuous Systems
Proceedings of the ITG/GI/GMM-Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", 2004 (pdf, bibtex)-
Using BDDs in a Branch & Cut Framework
4. International Workshop on Efficient and Experimental Algorithms (WEA'05), Santorini, Greece, LNCS 3503, Springer, p. 452-463, May 2005 (pdf, bibtex). The original publication is available at www.springerlink.com. -
Analysis of Large Safety-Critical Systems: A Quantitative Approach
Reports of SFB/TR 14 AVACS Nr. 8 (siehe www.avacs.org), 2006, ISSN 1860-9821 (pdf, bibtex) -
Minimization of Large State Spaces using Symbolic Branching Bisimulation
9. IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems, IEEE Computer Society Press, April 2006 (pdf, bibtex) -
Compositional Performability Evaluation for Statemate
3. International Conference on Quantitative Evaluation of Systems (QEST), IEEE Computer Society Press, Sept. 2006 (pdf, bibtex) -
Collaborative Exercise Management
Proceedings of the World Conference on E-Learning in Corporate, Government, Healthcare & Higher Education (E-LEARN), October 13-17, 2006 (pdf, bibtex) -
Sigref - A Symbolic Bisimulation Tool Box
4. International Symposium on Automated Technology for Verification and Analysis (ATVA), October 23-26, 2006, Beijing, China (pdf, bibtex) The original publication is available at www.springerlink.com. -
Forwarding, Splitting, and Block Ordering to Optimize BDD-based Bisimulation Computation
10. Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", March 5-7, 2007, Erlangen, Germany (bibtex) -
Optimization Techniques for BDD-based Bisimulation Computation
Proceedings of the 17th Great Lakes Symposium on VLSI, March 11-13, 2007, Stresa, Italy (bibtex) -
Towards Symbolic Stochastic Aggregation
Reports of SFB/TR 14 AVACS Nr. 16 (siehe www.avacs.org), 2007, ISSN 1860-9821 (pdf, bibtex) -
Symbolic Model Checking of DTMCs with Exact and Inexact Arithmetic
Reports of SFB/TR 14 AVACS Nr. 30 (siehe www.avacs.org), 2007, ISSN 1860-9821 (pdf, bibtex) -
The Demand for Reliability in Probabilistic Verification
11. Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" March 3-5, 2008, Freiburg, Germany (bibtex) -
Probabilistic Model Checking and Reliability of Results
11. IEEE International Workshop on Design and Diagnostics of Electronic Circuits and Systems, April 2008, Bratislava, Slovakia (pdf, bibtex) -
Symbolic Partition Refinement with Dynamic Balancing of Time and Space
5. International Conference on Quantitative Evaluation of Systems, September 2008, St. Malo, France (pdf, bibtex) -
Propositional Approximations for Bounded Model Checking of Partial Circuit Designs
26. IEEE International Conference on Computer Design, October 2008, Squaw Creek, CA, USA (pdf, bibtex) -
Counterexample Generation for Discrete-Time Markov Chains using Bounded Model Checking
10. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2009, Savannah, GA, USA, Volume 5403 of Lecture Notes in Computer Science, Springer-Verlag (pdf, bibtex). The original publication is available at www.springerlink.com. -
Compositional Dependability Evaluation for STATEMATE
IEEE Transactions on Software Engineering 35(2):274-292, 2009 (pdf, bibtex) -
Picoso - A Parallel Interval Constraint Solver
The 2009 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA), July 2009, Las Vegas, NV, USA (bibtex) -
Dependability Engineering of Silent Self-Stabilizing Systems
11. International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), November 2009, Lyon, France, Volume 5873 of Lecture Notes in Computer Science, Springer-Verlag (pdf, bibtex) The original publication is available at www.springerlink.com. -
Symbolic Partition Refinement with Automatic Balancing of Time and Space
Performance Evaluation, 67(9):815-835, 2010 (pdf, bibtex) -
Exploiting Different Strategies for the Parallelization of an SMT Solver
13. GI/ITG/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV), February 2010, Dresden, Germany, (bibtex) -
Correctness Issues of Symbolic Bisimulation Computation for Markov Chains
15. International GI/ITG Conference on Measurement, Modeling, and Evaluation of Computing Systems (MMB), March 2010, Essen, Germany, Volume 5987 of Lecture Notes in Computer Science, Springer-Verlag. (pdf, bibtex) The original publication is available at www.springerlink.com. -
A Model Checker for AADL
22. International Conference on Computer-Aided Verification (CAV), July 2010, Edinburg, UK (to appear) (pdf, bibtex) The original publication is available at www.springerlink.com. -
Bounded Fairness for Probabilistic Distributed Algorithms
Reports of SFB/TR 14 AVACS Nr. 57 (siehe www.avacs.org), 2010, ISSN 1860-9821 (pdf, bibtex) -
Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems
7. International Conference on Quantitative Evaluation of Systems (QEST), Sept. 2010, Williamsburg, VA, USA, IEEE Computer Society Press (pdf, bibtex) -
DTMC Model Checking by SCC Reduction
7. International Conference on Quantitative Evaluation of Systems (QEST), Sept. 2010, Williamsburg, VA, USA, IEEE Computer Society Press (pdf) -
On the Minimization of Hybrid Automata
22. Nordic Workshop on Programming Theory (NWPT), Nov. 2010, Turku, Finland -
Symbolische Methoden für die probabilistische Verifikation – Zustandsraumreduktion und Gegenbeispiele
PhD-thesis (dissertation), Jan. 2011 (pdf, bibtex) -
SMT-based Counterexample Generation for Markov Chains
14. Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV), February 2010, Oldenburg, Germany (bibtex) -
Counterexample Generation for Markov chains using SMT-based bounded model checking
13. IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS) / 31. IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems (FORTE), June 2011, Reykjavik, Iceland. (bibtex) -
Bounded Fairness for Probabilistic Distributed Algorithms
11. International Conference on Application of Concurrency to System Design (ACSD), June 2011, Newcastle Upon Tyne, United Kingdom, IEEE Computer Society Press. (bibtex) -
Reachability Analysis for Incomplete Networks of Markov Decision Processes
9. International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2011, Cambridge, United Kingdom, IEEE Computer Society Press. (bibtex) -
Hierarchical Counterexamples for Discrete-time Markov Chains
9. International Symposium on Automated Technology for Automatic Verification (ATVA), October 2011, Taipei, Taiwan, Springer-Verlag. -
Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties
15. Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV), March 2012, Kaiserslautern, Germany (to appear) (pdf, bibtex) -
Minimal Critical Subsystems for Markov Models
18. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), March 2012, Tallinn, Estonia (to appear) (pdf, bibtex) The original publication is available at www.springerlink.com.
2004
2005
2006
2007
2008
2009
2010
2011
2012
-
