Michael Weber

Postal Address:

RWTH Aachen
Lehrstuhl für Informatik II
D-52056 Aachen, Germany

Visiting Address:

RWTH Aachen
Lehrstuhl für Informatik II
Ahornstr. 55
D-52074 Aachen, Germany
Room: 4210 (building: E1, second floor)

Contact:

Office:  +49 241 80-21 240
Fax:     +49 241 80-22 217

Email: michaelw@i2.informatik.rwth-aachen.de

Personal

I am PhD student at the Chair for Computer Science II and a member of the Modelling Concurrent Systems Group.

For my PhD studies (which I started in March 2001), I received a scholarship from the graduate college 643 "Software für Kommunikationssysteme" until December 2002. Starting from January 2003, I am employed as regular staff member.

My research topic is Parallel Algorithms for Systems Verification.

Personal homepage, sort of... :-)

Research Interests

Model Checking
Protocol Verification
Semantics of Programming Languages

VMSSG, a Virtual Machine for state space generation

Publications

[1]	Michael Weber. Paralleles Model Checking. Diplomarbeit, Aachen, University of Technology, February 2001. (German). [ bib \| .ps.gz \| .pdf.gz ]
[2]	Benedikt Bollig, Martin Leucker, and Michael Weber. Parallel model checking for the alternation free mu-calculus. In Tiziana Margaria and Wang Yi, editors, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), volume 2031 of Lecture Notes in Computer Science, pages 543-558. Springer, April 2001. (superseded by BLW01a) [ bib ]
[3]	Benedikt Bollig, Martin Leucker, and Michael Weber. Local parallel model checking for the alternation free mu-calculus. Technical Report AIB-04-2001, RWTH Aachen, March 2001. [ bib \| .ps.gz \| Abstract ]
[4]	Benedikt Bollig, Martin Leucker, and Michael Weber. Local parallel model checking for the alternation-free mu-calculus. In Proceedings of the 9th International SPIN Workshop on Model checking of Software (SPIN '02), Lecture Notes in Computer Science. Springer-Verlag Inc., 2002. [ bib \| .pdf ]
[5]	Martin Leucker, Rafal Somla and Michael Weber. Parallel model checking for LTL, CTL* and L_μ². In Lubos Brim and Orna Grumberg, editors, Electronic Notes in Theoretical Computer Science (ENTCS), volume 89. Elsevier Science Publishers, 2003. [ bib \| .ps.gz \| .pdf ]
[6]	Manuel Chakravarty (editor), Sigbjorn Finne, Fergus Henderson, Marcin Kowalczyk, Daan Leijen, Simon Marlow, Erik Meijer, Sven Panne, Simon Peyton Jones, Alastair Reid, Malcolm Wallace, and Michael Weber. The Haskell Foreign Function Interface 1.0. 2003. [ .ps.gz \| .pdf ]
[7]	Martin Leucker, Thomas Noll, Perdita Stevens, and Michael Weber. Functional programming languages for verification tools: A comparison of ML and Haskell. Software Tools for Technology Transfer, 7(2):184–194, 2005. [ .pdf \| DOI ]
[8]	M. Leucker, M. Weber, V. Forejt, and J. Barnat. DivSPIN -- A SPIN compatible distributed model checker. PDMC 2005 short presentation. [ .ps ]
[9]	Michael Weber, Stefan Schürmans. A Virtual Machine for State Space Generation. submitted, draft copy.

Attended Conferences, Summer Schools, etc.

Implementation of Functional Languages, 12th International Workshop (IFL2000), 4-7 September 2000, Aachen, Germany
ETAPS 2001, 2-6 April 2001, Genova, Italy
18. Workshop der GI-Fachgruppe 2.1.4 Programmiersprachen und Rechenkonzepte, 7-9 May 2001, Bad Honnef, Germany
Given talk: "HaskellMPI - Entwicklung paralleler Programme in Haskell" (Abstract)
1st International School on Formal Methods for the Design of Computer, Communication and Software Systems: Process Algebras (SFM-01:PA), 23-28 July 2001, Bertinoro, Italy
Invited talk: Tool Demo Truth
3rd Scottish Functional Programming Workshop (SFP'01), 22-24 August 2001, Stirling, Scotland
Given talk: "Functional Programming Languages for Verification Tools: Experiences with ML and Haskell" (paper with Martin Leucker, Thomas Noll, Perdita Stevens)
Kolloquium Programmiersprachen und Grundlagen der Programmierung (Rurberg'01), 7-11 October 2001, Rurberg, Germany
SPIN 2002 (satellite event of ETAPS 2002), 11-13 April 2002, Grenoble, France
Given talk: "Local Parallel Model Checking for the Alternation Free mu-calculus"
SFEDL 2002 (satellite event of ETAPS 2002), 14 April 2002, Grenoble, France
NATO Advanced Study Institute on Models, Algebras, and Logic of Engineering Software, 30 July - 11 August 2002, Marktoberdorf, Germany
Research visit at ParaDiSe Labs, Prof. Luboš Brim, Masaryk University, 15-19 November 2004, Brno, Czech Republic.
ETAPS 2005, 2-9 April 2005, Edinburgh, Scotland.
22. Workshop der GI-Fachgruppe 2.1.4 Programmiersprachen und Rechenkonzepte, 2-4 May 2005, Bad Honnef, Germany
Given talk: "A Virtual Machine for State Space Generation" (Abstract)
SENVA 2005 workshop, 30 May - 1 June 2005, Saint Pierre de Chartreuse (Isère), France
Invited Talk: "Parallel Model Checking (for mu-Calculus with upto one Alternation)"
Invited Talk: "State Space Generation Revisited"

Teaching Activities

I have taught, prepared, and helped to prepare seminars, labs and courses, and I also offer diploma theses to students.

Courses

2001 (winter term): Proseminar Websprachen (co-organizer/tutor)
2002 (winter term): Seminar Verifikation von Programmen (tutor)
2002 (summer term): Proseminar IT-Sicherheitskonzepte und Sicherheit in Java (tutor); Seminar Message Sequence Charts (tutor); Seminar Deklarative Programmiersprachen (tutor)
2002 (winter term): Proseminar Spezifikationssprachen für Verteilte Systeme (tutor)
2003 (summer term): Lab Compilerbau (organizer); Seminar Compilerbau (tutor); Proseminar IT-Sicherheitskonzepte und Sicherheit in Java (tutor)
2003 (winter term): Short Course Einführung in LaTeX (lecturer); Proseminar Websprachen (organizer/sole tutor); Seminar Analyse und Optimierung imperativer und funktionaler Programme (tutor)
2004 (summer term): Course Compilerbau; Seminar Logikprogrammierung (tutor); Proseminar IT-Sicherheitskonzepte und Sicherheit in Java (tutor)
2004 (winter term): Short Course Einführung in LaTeX (lecturer); Lab Compilerbau (organizer); Seminar Message Sequence Charts (tutor); Proseminar Programmiersprachen (organizer)
2005 (summer term): Seminar Modelling, Analysis, and Optimization of Object-Based Systems (tutor); Proseminar Fortgeschrittene Programmierkonzepte in Java, Haskell und Prolog (tutor)
2005 (winter term): Lab Compilerbau (organizer)

Available Diploma Theses

Reverse-Engineering von UML-Spezifikationen aus Java-Programmen (in German), Martin Keschenau
Status: finished (2004), First place at OOPSLA2004's Student Research Competition.
A Compiler and Virtual Machine for State Space Generation (in German), Stefan Schürmans
Status: finished (2005)
Static Byte-code Analysis for State-space reduction (in German), Gustavo Quiros
Status: finished (2006)
Model Checking of Embedded Systems Software (in German), Michael Rohrbach, in cooperation with Lehrstuhl Informatik XI (Embedded Software Group)
Status: on-going

Webmaster

Disclaimer

Last modified: 2006-07-07 14:32 UTC