Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Student Projects

Master/Diploma Theses
A solver for a theory of strings
(in cooperation with mgm technology partners GmbH)
( PDF Description )
DoneStatus: Finished
Contact: esparza@in.tum.de
Supervisor: Javier Esparza
Efficient verification of multi-threaded programs
DoneStatus: Finished
Thesis DownloadDownload Thesis
Contact: popeea@model.in.tum.de
Supervisor: Andrey Rybalchenko
Advisor: Corneliu Popeea
Higher-Order Model-Checking and Underapproximate Models of Concurrent Recursive Programs
( PDF Description )
DoneStatus: Finished
Contact: broadben@in.tum.de
Supervisor: Christopher Broadbent
Advisor: Javier Esparza
Kleene Theorem generalized to Regular Word Transformations
( PDF Description )
DoneStatus: Finished
Contact: durandga@in.tum.de
Supervisor: Antoine Durand-Gasselin
Advisor: Javier Esparza
Provably Correct Implementations of Algorithms for Elliptic Curve Cryptography using Isabelle/HOL
DoneStatus: Finished
Contact: luttenbe@model.in.tum.de
Supervisor: Michael Luttenberger
Advisor: Javier Esparza
Symbolic Representations of Semilinear Sets
( PDF Description )
DoneStatus: Finished
Thesis DownloadDownload Thesis
Contact: schlund@model.in.tum.de
Supervisor: Javier Esparza
Advisor: Maximilian Schlund


Bachelor Theses
A Tool for Modal Transition Systems
( PDF Description )( Further Information )
DoneStatus: Finished
Thesis DownloadDownload Thesis
Thesis Presentation DownloadDownload Presentation
Thesis Material DownloadDownload Material
Contact: jan.kretinsky@in.tum.de
Supervisor: Javier Esparza
Advisor: Jan Kretinsky
A Tool for Verification and Simulation of Population Protocols
DoneStatus: Finished
Thesis DownloadDownload Thesis
Thesis Presentation DownloadDownload Presentation
Contact: blondin@in.tum.de
Supervisor: Javier Esparza
Advisor: Michael Blondin
An Advanced Solver for Presburger Arithmetic
( PDF Description )( Further Information )
DoneStatus: Finished
Thesis DownloadDownload Thesis
Contact: esparza@in.tum.de
Supervisor: Javier Esparza
Master Z-Automata for Regular Languages
DoneStatus: Finished
Thesis DownloadDownload Thesis
Thesis Material DownloadDownload Material
Contact: esparza@in.tum.de
Supervisor: Javier Esparza
Probabilistic cellular automata
( PDF Description )
DoneStatus: Finished
Thesis DownloadDownload Thesis
Thesis Presentation DownloadDownload Presentation
Contact: jan.kretinsky@in.tum.de
Supervisor: Javier Esparza
Advisor: Jan Kretinsky
Small deterministic Omega­ Automata for LTL: A second generation implementation.
( PDF Description )( Further Information )
DoneStatus: Finished
Contact: sickert@in.tum.de
Supervisor: Salomon Sickert
Advisor: Javier Esparza
Strategy Iteration on the Graphics Card
( PDF Description )
DoneStatus: Finished
Thesis DownloadDownload Thesis
Contact: luttenbe@model.in.tum.de
Supervisor: Javier Esparza
Advisor: Michael Luttenberger
Upper Bounds for Policy-Iteration Sequences
( PDF Description )
DoneStatus: Finished
Contact: luttenbe@model.in.tum.de
Supervisor: Javier Esparza
Advisor: Michael Luttenberger


Master/Diploma or Bachelor Theses
A Tool for Regular Real Analysis
( PDF Description )
DoneStatus: Finished
Contact: schlund@model.in.tum.de
Supervisor: Maximilian Schlund
Advisor: Javier Esparza
Attacks on Hard Grammar Problems
( PDF Description )
DoneStatus: Finished
Contact: schlund@model.in.tum.de
Supervisor: Maximilian Schlund
Advisor: Javier Esparza