My Personal Page: Jan Tobias Mühlberg

contact | brief | publications | projects | friends | disclaimer

Me/Contact There's something special about me. Of course I won't tell you :-) current occupation: senior staff scientist at the University of Bamberg, Software Technologies Research Group previously: grad student at the University of York, PLASMA Research Group; researcher at the University of Applied Sciences in Brandenburg e-mail: jtmuehlberg@gmail.com pgp-key: muehlber.asc; available on public keyservers keyid: 1024D/5BC905EC 2002-03-20 fingerprint: 9DC9 9968 98D5 3673 5C57 A98B 930B AF48 5BC9 05EC phone: Don't call me! Please write an e-mail instead! ++49 (0)951 8633854 (office in Bamberg) ++44 (0)1904 432710 (office in York) ++49 (0)951 5195987 (home) Beware! LinkedIn: http://uk.linkedin.com/pub/jan-tobias-muehlberg/6/2A0/754 Facebook: http://www.facebook.com/jtmuehlberg further contact information is available here and here. Interests Computer Science: automated software engineering and software verification, model checking, semantics, program analysis and program abstraction, memory models and heap abstraction, analysis of object code programs, security protocols, cryptography Biology/Entomology: mainly Chrysomelidae and Silphidae Hobbies: far too many -- I'm changing them from time to time

"Nach dem Aufstand des 17. Juni Ließ der Sekretär des Schriftstellerverbandes In der Stalinallee Flugblätter verteilen Auf denen zu lesen war, daß das Volk Das Vertrauen der Regierung verscherzt habe Und es nur noch durch verdoppelte Arbeit Zurückerobern könne. Wäre es da Nicht einfacher, die Regierung Löste das Volk auf und Wählte ein anderes?" -- Bertolt Brecht, "Die Lösung"

In brief: Research and Teaching

• Publications on DBLP (there's a full list including technical reports and talks below)
• Topics for YOUR final year project (Diplom-/Master-/Bachelorarbeit):
  • "Developing & Implementing a Property Specification Language for SOCA"; "Developing & Implementing a GDB Front-End for SOCA"; "SOCA GUI Development" (full description)
  • Older topics I might still be interested in: "Evaluierung der Praxistauglichkeit von Werkzeugen zur Software-Verifikation"; "Objekt-Code-Slicing zur Verifikation von Pointer-Programmen" (full description)
• Demonstrating and Teaching at the University of Bamberg:
  • Software Engineering, Compiler Construction, Requirements Engineering, Automated Verification, Programming in C
  • Course notes are available at Bamberg only
• Demonstrating and Teaching at the University of York, until May 2009:
  • Protocol Design and Validation, Requirements Engineering, Reactive Systems Design, Mathematics for Computer Science
  • Course notes are available at York only
• Teaching at the Fachhochschule Brandenburg, until October 2005:
  • WI-Propädeutikum zum Thema Linux (FHB/WI, Wintersemester 2005/06)
  • WI-Propädeutikum zum Thema LaTeX (FHB/WI, Wintersemester 2005/06)
  • Wahlpflichtfach "Sicherheitsmanagement in der IT" (FHB/WI, Sommersemester 2005)
  • Gastvorträge im Fach "Medienwirtschaft" (FHB/FBI, Sommersemester 2005)
  • Lehrangebote zur Schulkooperation mit dem OSZ "Alfred Flakowski" (FHB, Sommersemester 2005)
  • WI-Propädeutikum zum Thema LaTeX (FHB/WI, Wintersemester 2004/05)
  • Wahlpflichtfach "Sicherheitsmanagement in der IT" (FHB/WI, Wintersemester 2004/05)
  • Gastvorträge im Wahlpflichtfach "E-Government in der Praxis" (FHB/WI, Wintersemester 2004/05)

Seminar Papers, Presentations, Essays, etc.

	Document in German			Document in English			Unclassified stuff			A piece of code
	Scientific paper			Essay or similar			Short stuff for newspapers			Talk/Slides

• Publications on DBLP

• coming soon:       "Verifying Compiled File System Code" -- Jan Tobias Mühlberg and Gerald Lüttgen; Formal Aspects of Computing -- Applicable Formal Methods (FACJ): bibtex
• coming soon:       "Symbolic Object Code Analysis" -- Jan Tobias Mühlberg and Gerald Lüttgen; 17th International SPIN Workshop on Model Checking of Software (SPIN 2010), 27th to 29th September 2010: bibtex
• "Model Checking Pointer Safety in Compiled Programs" -- Jan Tobias Mühlberg; PhD Thesis, Department of Computer Science, University of York, September 2009: pdf, bibtex (also available at whiterose.ac.uk)
• "Parallelization of Decision Procedures" -- Alexander Ditter and Jan Tobias Mühlberg; D-CON 2010, Introduction to a discussion session on parallel SMT solving, University of Bamberg, 04th March 2010: abstract (txt), slides (pdf)
• "Symbolic Object Code Analysis" -- Jan Tobias Mühlberg and Gerald Lüttgen; Technical Report 85/2010, Faculty of Information Systems and Applied Computer Sciences, The University of Bamberg, February 2010: pdf, bibtex, OPUS
• "Symbolic Object Code Analysis" -- Jan Tobias Mühlberg and Gerald Lüttgen; Monday Afternoon Club, University of Bamberg (MAC 2009/2010); 25th January 2010: pdf
• "Wie bleibt unser Geheimnis geheim?" -- Jan Tobias Mühlberg, slides for a workshop on cryptoraphy for girls at the age of 10 to 14 ("Mädchen und Technik"), University of Bamberg, November 4th 2009: abstract (txt), slides (pdf)
• "Verifying Compiled File System Code" -- Jan Tobias Mühlberg and Gerald Lüttgen; Brazilian Symposium on Formal Methods (SBMF 2009); 21st August 2009: pdf
• "Verifying Compiled File System Code" -- Jan Tobias Mühlberg and Gerald Lüttgen; Brazilian Symposium on Formal Methods (SBMF 2009); August 2009: pdf, bibtex
• "Model-Checking the Linux Virtual File System" -- Andy Galloway, Gerald Lüttgen, Jan Tobias Mühlberg and Radu Siminiceanu; Verification, Model Checking, and Abstract Interpretation (VMCAI 2009); January 2009: pdf, bibtex, additional material
• "Is Your Program Memory Safe? -- Can we use bounded model checking to find memory safety violations in compiled programs?" -- Thesis Seminar given on 10th July 2008 in York: pdf
• "Slicing Object Code -- and finding memory safety violations" -- talk given at a PLASMA seminar in York on 28th February 2008 and in a Theory-Seminar in Birmingham on 29th February 2008: pdf, abstract
• scade2brick -- I'm back to playing with Lego and SCADE, and hence there's a new release of scade2brick. It's supporting rotation sensors now: website
• "Model Checking Linux's Virtual File System" -- talk on the report below, given at the Workshop on the Verifiable File Store Mini-Challenge (part of Grand Challenge 6: Dependable Systems Evolution), 18th December 2007, BCS HQ, London: pdf (I gave this talk a second time in the HISE-seminar on 04th March 2008 in York)
• "Model-checking Part of a Linux File System" -- Andy Galloway, Jan Tobias Mühlberg, Radu Siminiceanu and Gerald Lüttgen; Technical Report YCS-2007-423, Department of Computer Science, University of York, UK, November 2007: pdf, bibtex, additional material
• "Proceedings of the 1st York Doctoral Symposium on Computing" -- Jan Tobias Mühlberg and Juan Ignacio Perna, Technical Report YCS-2007-421, Department of Computer Science, University of York, UK, October 2007: pdf, bibtex
• "FUN with Lego Mindstorms" -- PLASMA talk given together with Matthew Naylor on 01 March 2007: pdf, abstract. Matthew wrote a nice paper on "Behavioural Circuit Design in Lava" which covers the second part of this talk in detail. It's published in issue 7 of The Monad.Reader. Just the article: pdf
• "Towards a Simulation-based Verification of Memory Safety Properties for Object Code Programs" -- PLASMA talk given on 22 February 2007: pdf, abstract
• "Studie zum Innovationsverhalten deutscher Software-Entwicklungsunternehmen" -- A study commissioned by the Federal Ministry of Education and Research of Germany, December 2006, authored by Friedrich-L. Holl, Katharina Menzel, Peter Morcinek, Jan Tobias Mühlberg, Ingo Schäfer and Hanno Schüngel: pdf, bibtex
• "Metastudie Open-Source-Software und ihre Bedeutung für Innovatives Handeln" -- A study commissioned by the Federal Ministry of Education and Research of Germany, December 2006, authored by Hartmut Heinrich, Friedrich Holl, Katharina Menzel, Jan Tobias Mühlberg, Ingo Schäfer and Hanno Schüngel: pdf, bibtex
• "Elliptische Kurven und Kryptographie" -- An introduction to Elliptic Curve Cryptography, given together with Arnd Zapletal on 21 December 2006. There are only slides for the first part of the talk. The second half of it was given by Arnd on the blackboard: pdf
• scade2brick -- Prepare C code generated by SCADE for compilation with brickOS: website
• "Securing Your E-Mail" -- Yet another talk on cryptography and GnuPG, given on 17 October 2006: abstract, slides
• "Validating and Verifying Memory Safety for Concurrent Operating System Code" -- PhD Qualifying Dissertation, unfinished version: pdf
• "BLASTing Linux Code" -- a paper and related stuff for FMICS 2006, co-authored by Gerald Lüttgen: additional material, pdf, bibtex
• "Programme aus Quellen" -- this workshop held by MaD and me on BLIT 2006 has a really strange title. However, related material can be found here.
• "Software Property Checking" -- a few slides for a presentation on software verification; held in the PLASMA meeting on 9 March 2006: pdf
• A not so short talk on LaTeX, 09. January 2006: LaTeX -- Belegarbeiten in schön
• I'm preparing a workshop for 22C3. The topic is "OSS: Reliability and Maintainability?" -- I'm going to provide some further material in advance of the event here.
• "Automated Verification of Operating System Code" -- slides for a literature review presentation held on 19 December 2005 in York: pdf
• "Software-Engineering und Software-Qualität in Open-Source-Projekten" published in Open Source Jahrbuch 2006: pdf bibtex
• "What have you designed today? -- Software Quality in Open Source Projects" -- slides for a presentation on an interesting part of one of my former research projects: pdf
• "Wird der Hochschulstandort Brandenburg unattraktiv?" -- an attempt to discuss the relation between the University of applied Sciences in Brandenburg an the city of Brandenburg on the example of the Semesterticket; published in Scheinwerfer 03/2005, October 2005: html pdf
• There's a new (German) paper and a corresponding set of slides showing what CIDAS is and how it works. It was written in July 2005: paper slides (both pdf)
• "Studentische Projekte: Freie Studenten für Freie Software" -- Es ist gemeinhin falsch zu schreiben, was man nicht machen soll. Aber es ist oftmals schwer, die Dinge anders auszudrücken. Erschienen mit vielen Rechtschreib- und Satzfehlern im Scheinwerfer 02/2005; Juni 2005: html pdf
• "Object Code-Near Software Verification" -- an approach on doing formal software verification slightly different from the usual way: pdf
• Keynote zum Brandenburger Linux-Infotag 2005, "Mit Freier Software die Welt verändern!", 23. April 2005: pdf
• Keynote zum Brandenburger Linux-Infotag 2005, "Warum Freie Software? Im Mittelstand?", 22. April 2005: pdf
• This isn't a paper or presentation at all. Some friends asked me to to write an empty but almost complete example for diploma thesis or more substantial seminar papers in LaTeX. Actually all I did was to remove the contents of my own diploma and filled it up with some nonsense. Hopefully it's of some use for them. Here we go: pdf view files tar.gz
• BraLUG-Vortrag im März 2005, "Kryptographie -- Eine Einführung", ein unglaublich kurzer und inhaltlich dementsprechend sehr ungenauer Vortrag. Aber manchmal scheint es einfach besser zu sein, die Mathematik wegzulassen: pdf
• Vortrag zur Brandenburg Clusternight im Januar 2005, "Aus Zahlen werden Bilder": pdf
• "Mementoes." -- a bunch of thoughts about privacy written for a bunch of people who don't care on the privacy of their own children at all: html
• "Kein Freibier!" -- some thoughts about Free Information and Free Education, published in Scheinwerfer 01/2005, January 2005: html pdf
• "Interview: Für 29.-- Euro nach Bologna" -- Interview mit Prof. Dr. Hoier, neuer Vizepräsident für Lehre und Studium an der Fachhochschule Brandenburg; erschienen im Scheinwerfer 01/2005, Januar 2005: pdf
• BraLUG-Vortrag im November 2004, "GNU/Linux -- Eine Einführung": pdf
• Der "Italienische Kerzenleuchter" -- Wahrheit oder Mythos? html
• Vortrag bei der IHK-Potsdam im November 2004, "Was bedeutet Linux für den Mittelstand": pdf
• "Interview: Evaluation der Lehre an der FHB" -- Interview mit Prof. Dr. Lüthy, ehemals Senatorin an der Fachhochschule Brandenburg; erschienen im Scheinwerfer 04/2004, September 2004: pdf
• "Interview: Er hat Jehova gesagt!" -- Interview mit Prof. Dr. Holl, dem ehemaligen Vorsitzenden des Senates der Fachhochschule Brandenburg; erschienen im Scheinwerfer 03/2004, Juni 2004: pdf
• Some slides about CIDAS used for several presentations since February 2004: german, english (both pdf)
• Diplomarbeit und Vortragsfolien, Mai 2004, "Konzeption und prototypische Umsetzung von Authentifizierungsverfahren und Kommunikationsschnittstellen für das Identity-Management-System CIDAS unter besonderer Berücksichtigung mobiler identifizierbarer Datenträger": task.pdf, diplom.pdf, coll-slides.pdf, coll-poster.pdf
• BraLUG-Vortrag im Dezember 2003, "OpenPGP": pdf
• BraLUG-Vortrag im Dezember 2003, "Kryptographie -- Eine Einführung", This set of slides is not exhaustive. I wrote it as an introduction for one of my presentation about e-mail security and OpenPGP. Therefore it only points out some basic points about cryptographic systems being used: pdf
• Belegarbeit Datensicherheit, WiSe 2003, "Viren und Würmer unter UNIX", Autoren: Hannes Seidel, Jan Tobias Mühlberg: pdf tex
• Belegarbeit Applikationen Intelligenter Systeme, WiSe 2003, "Erstellung einer Kompasskarte mit dem Pioneer II", Autoren: Jan Tobias Mühlberg, Hannes Seidel: pdf tex data
• "MUDs: Textorientierte Rollenspiele auf dem Computer", February 2002, I don't remember what I wrote this paper for...: pdf tex
• Belegarbeit Interaktive Dramaturgien, Drehbücher und Filme, WiSe2002, "Kartenentwurf für Caesar III -- Brendanburg": pdf tex map
• Belegarbeit Gesellschaftliche Aspekte der Informatik, SoSe2002, "Von Menschen, Tieren und Mülltonnen", This is only my part of the essay collection above. No idea, why I'm keeping a separate copy.: pdf tex
• Belegarbeit Gesellschaftliche Aspekte der Informatik, SoSe2002, "Kybernetik", Autoren: André Adam, Martin Krüger, Jan Tobias Mühlberg, Alexander Schulte, Hannes Seidel: pdf tex
• Belegarbeit Alternative Programmiersprachen, SoSe2002, "Affen und Gnus -- Implementierungen von Microsofts .NET-Framework unter GNU/Linux": pdf tex
• Belegarbeit Datenbankprogrammierung, SoSe2002: pdf tex sources
• Vortragsbegleitendes Material, WiSe 2002, "Virtual Private Networks", Autoren: Markus Dahms, Jan Tobias Mühlberg: pdf tex

Projects/Activitiesi

• D-CON
• York Doctoral Symposium
• BraLUG -- Brandenburger Linux User Group e.V.
• YLUG -- York Linux User Group; same as the above but for my current working location.
• Förderverein Großtrappenschutz e.V. -- unfortunately I can't spend as much time in environmental protection as I want to.
• INNODES -- "Innovationsverhalten deutscher Software-Entwicklungsunternehmen"
• Within the project INNODES, a meta study on open source software has been developed. We provide access to the current state of the bibliography and annotations using a tool called BibDB The database can be accessed at http://innodes.fh-brandenburg.de/bibdb/.
• "Kultur machen" -- just lacking time... :-(
• Scheinwerfer -- Die studentische Zeitung an der FH-Brandenburg (there is a secondary website available)
• BLIT -- Brandenburger Linux-Infotag (annual event organised by the school of Computing and Media and the BraLUG).
• Brandenburg Clusternight -- not an annual event but we may repeat it in case we have something to calculate. We really thank the University of Applied Sciences in Brandenburg and the Institute for Computer Science at the University Potsdam for help and support.
• CIDAS -- Configurable Internet Directory and Authentication Service. This project has been abandoned.

Nice gals and guys

• Los Comandantes -- You've to put on a barett with a red star for their concerts!
• Der Jannixx ihr Blog. -- Die hat's nach Bournemouth verschlagen. Und ihr Blog traegt noch den illusorischen Titel "PhD 2009". Naja, so optimistisch waren wir ja alle mal :-)
• Tanja Miethe -- Sie wäre gerne süß und niedlich, aber ich muß ihr immer sagen, daß sie dafür zu groß ist. Aber toll isse trotzdem. Und sie kann besser berlinern als ich.

contact | brief | publications | projects | friends | disclaimer