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
Extension of a GPU-based solver for Parity Games
( PDF Description )
AvailableStatus: Available
Contact: luttenbe@model.in.tum.de
Supervisor: Michael Luttenberger
Advisor: Javier Esparza
Higher-Order Model-Checking and Underapproximate Models of Concurrent Recursive Programs
( PDF Description )
AvailableStatus: Available
Contact: broadben@in.tum.de
Supervisor: Christopher Broadbent
Advisor: Javier Esparza
Kleene Theorem generalized to Regular Word Transformations
( PDF Description )
AvailableStatus: Available
Contact: durandga@in.tum.de
Supervisor: Antoine Durand-Gasselin
Advisor: Javier Esparza
Provably Correct Implementations of Algorithms for Elliptic Curve Cryptography using Isabelle/HOL
AvailableStatus: Available
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
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 )
AssignedStatus: Assigned
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 )
AssignedStatus: Assigned
Contact: schlund@model.in.tum.de
Supervisor: Maximilian Schlund
Advisor: Javier Esparza
Attacks on Hard Grammar Problems
( PDF Description )
AssignedStatus: Assigned
Contact: schlund@model.in.tum.de
Supervisor: Maximilian Schlund
Advisor: Javier Esparza