Marius Greitschus

University of Freiburg

Georges-Köhler-Allee 52

79110 Freiburg

building 052, room 00-005

+49 761 203 8248

greitsch@informatik.uni-freiburg.de

Research Interests

Abstract Interpretation
Static Checking
Software Verification
Software Design
Software Engineering
Verification Techniques for Hybrid Systems

Publications

Loop Invariants from Counterexamples, Static Analysis Symposium (SAS 2017), together with Daniel Dietsch and Andreas Podelski. [ Springer | dblp ]
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata (Competition Contribution), Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), together with Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling, Frank Schüssele, and Andreas Podelski. [ Springer | dblp ]
Ultimate Taipan: Trace Abstraction and Abstract Interpretation (Competition Contribution), Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), together with Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Schätzle, Christian Schilling, Frank Schüssele, and Andreas Podelski. [ Springer | dblp ]
Ultimate Automizer with Two-Track Proofs (Competition Contribution), Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), together with Matthias Heizmann, Daniel Dietsch, Jan Leike, Betim Musa, Claus Schätzle, and Andreas Podelski. [ Springer | dblp ]
Co-Simulation of Hybrid Systems with SpaceEx and Uppaal, 11th International Modelica Conference (Modelica 2015), together with Sergiy Bogomolov, Peter G. Jensen, Kim G. Larsen, Marius Mikučionis, Thomas Strump and Stavros Tripakis. [ pdf ]
Benchmark: Stratified Controllers of Tank Networks, Applied Verification of Continuous and Hybrid Systems (ARCH 2015), together with Stanley Bak, Sergiy Bogomolov, and Taylor Johnson. [ pdf & BibTex ]
Eliminating Spurious Transitions in Reachability with Support Functions, 18th International Conference on Hybrid Systems: Computation and Control (HSCC 2015), together with Goran Frehse, Sergiy Bogomolov, Thomas Strump, and Andreas Podelski. [ ACM | dblp ]
Assume-Guarantee Abstraction Refinement Meets Hybrid Systems, 10th Haifa Verification Conference HVC2014, together with Sergiy Bogomolov, Goran Frehse, Radu Grosu, Corina Pasareanu, Andreas Podelski, and Thomas Strump. Winner of the Best Paper Award. [ Springer | dblp | pdf ]

Thesis

Combining Value Analysis and Static Checking for Automated Verification of Software Specifications. Master's Thesis, University of Freiburg, 2012.

Consultation Hours

Please contact me for an appointment or visit me at the office without an appointment (at the risk of being rejected).

Student Projects and Thesis Topics

Please see our shared overview for thesis topics and student projects. Additionally, if you have your own interesting topic you would like to work on and need a supervisor for, feel free to contact me.

Teaching

Seminar: Automata Theory (Winter Term 2017/2018)
Seminar: Formal Methods for C (Summer Term 2014)
Software Lab (Summer Terms 2013, 2014, 2015, 2016, 2017)
Software Lab for members of all faculties (Winter Terms 2012/2013, 2013/2014, 2014/2015, 2015/2016, 2016/2017, 2017/2018)

Tutoring

Software Lab (Summer Terms 2010, 2011, 2012)
Software Lab for members of all faculties (Winter Terms 2009/2010, 2010/2011, 2011/2012)

Supervised Student Projects and Theses

2018

Ingold, M.: Entwurf und Implementierung von Analysealgorithmen zum Handeln mit Aktien. Master's Project.
Heinz, A.: CEGAR and SMT for Planning. Master's Thesis.

2017

Jarecki, J.: Active Verification: Putting the User in the Loop. Master's Thesis.
Höck, M.: Entwurf und Implementierung einer Software für den automatischen Handel mit Aktien. Bachelor's thesis.
Löffler, J.: Hybrid Automata Support for the Ultimate Framework. Bachelor's Thesis.
Heinz, A.: Optimized Plan Extraction with MCTA, Master's Project.
Löffler, J.: SOCIS - The ESA Summer of Code in Space, Project.

2016

Jarecki, J.: Implementation of a Virtual Reality Graph Visualization and Manipulation Tool. Master's teamproject.
Burkart, M.: Visualization and Comparison of 3D-Pathfinding. Bachelor's thesis.
Braun, J.: Softwareprojekt zur Entwicklung eines Handyspiels mit Physik. Undergraduate project.
Schätzle, C.: An Octagon Abstract Domain For Ultimate. Bachelor's thesis.
Burkart, M., Dippel M.: Design and Implementation of a Game Engine. Bachelor's project.

2015

Strump, T.: Analysis Framework for Heterogeneous Dynamic Systems. Master's thesis.
Hättig, J.: Convex Polyhedra as Abstract Domain for Abstract Interpretation in Ultimate. Master's thesis.
Enke, J.: Flattening of Parallelly Composed Hybrid Automata. Bachelor's project.

2014

Dillo, C.: Modular Abstract Interpretation for Ultimate. Bachelor's thesis.
Richter, A.: Automated Medication Assurance. Bachelor's thesis.
Cheng N., Hättig J., Holub J., Schillinger F.: Advanced Video Game Architecture. Master's teamproject.

2013-2014

Dillo, C.: SpaceEx to Boogie. Bachelor's project.
Jayakumar, V.: Continuous Delivery for Small Java Web Based Applications. Master's thesis.
Meinke, J., Saier, D.: Dynamic Parameter Tuning for Hybrid Systems. Bachelor's project.
Rebmann, J., Ganz, S.: Implementation of a Benchmark Generator for Hybrid Systems. Bachelor's project.
Strump, T.: Location Merging for Hybrid Systems. Master's teamproject.

2012

Hofmann, C.: Verification as a Service. Bachelor's thesis.