Postal Address:
Michael Weber
University of Twente (EEMCS)
Formal Methods and Tools
P.O. Box 217
7500AE Enschede
The Netherlands
Visiting Address (Directions):
University of Twente
Zilverling (Room: 5037)
7522NB Enschede
The Netherlands
Available Projects! (Access restricted to UT network)
TSConIT 12 Project Proposals! (Access restricted to UT network)
| [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μ2.
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. Parallel
Algorithms for Verification of Large Systems.
Phd. thesis, AIB-2006-02, RWTH Aachen University, 2006.
[ bib | .pdf | .ps.gz | Abstract ] |
| [10] |
B. Schlich, M. Rohrbach, Michael Weber, and S. Kowalewski.
Model Checking Software for Microcontrollers.
Technical report AIB-2006-11, RWTH Aachen University, 2006.
[ bib | .pdf | .ps.gz | Abstract ] |
| [11] |
Moritz Hammer, Michael Weber.
To Store or Not to StoreReloaded: Reclaiming Memory on Demand. In L. Brim, B. Haverkort, M. Leucker, and J. van de Pol, editors, Formal Methods: Applications and Technology, volume 4346 of Lecture Notes in Computer Science, pages 51–66. Springer, August 2006. (EASST Best Paper Award) [ .pdf | Abstract ] |
| [12] |
Michael Weber.
An Embeddable Virtual Machine for State Space Generation.
In D. Bosnacki and S. Edelkamp, editors, Proceedings of SPIN 2007, volume 4595 of Lecture Notes
in Computer Science, pages 168–185. Springer.
[ .pdf | Abstract ] |
| [13] |
Stefan Blom, Bert Lisser, Jaco van de Pol, and Michael Weber.
A Database Approach to Distributed State Space Generation.
In B. Haverkort and I. Cerna, editors, Proceedings of PDMC 2007, ENTCS, to appear.
[ .pdf | Abstract ] |
| [14] |
Jirí Barnat, Luboš Brim, Pavel Šimeček, and Michael Weber.
Revisiting
Resistance Speeds Up I/O-Efficient LTL Model Checking.
In C.R. Ramakrishnan, Jakob Rehof, editors, Proceedings of TACAS 2008, volume 4963
of Lecture Notes in Computer Science, pages 48–64, to appear.
[ .pdf | Abstract ] |
| [15] |
Jaco van de Pol and Michael Weber.
A Multi-Core Solver for Parity Games.
In Ivana Černa and Gerald Lüttgen, editors, Proceedings of PDMC 2008, ENTCS, to appear.
[ .pdf | Abstract ] |
| [16] | S. Blom, B. Lisser, J. van de Pol, and M. Weber. A Database Approach to Distributed State-Space Generation. J Logic Computation, (to appear in print), 2009. |
| [17] | S.C.C. Blom, J.C. van de Pol, and M. Weber. Bridging the Gap Between Enumerative and Symbolic Model Checkers. Technical Report TR-CTIT-09-30, University of Twente, Enschede, June 2009. |
| [18] | M. Weber. An Embeddable Virtual Machine for State Space Generation. Software Tools for Technology Transfer, 2010. Invited publication, to appear. |
| [19] | S.C.C. Blom, J.C. van de Pol, and M. Weber. LTSmin: Distributed and Symbolic Reachability. CAV 2010 |
| [20] | A.W. Laarman, J.C. van de Pol, and M. Weber. Boosting Multi-Core Reachability Performance with Shared Hash Tables. FMCAD 2010 |
| [21] | A.W. Laarman, J.C. van de Pol, and M. Weber. Multi-Core LTSmin: Marrying Modularity and Scalability. NFM 2011 |
To Store or Not To StoreReloaded: Reclaiming Memory on Demand
VeriGEM: A Verification Grid for Enhanced Model Checking
I have taught, prepared, and helped to prepare seminars, labs and courses, and I also offer Diploma and Master's theses to students.