Ultimate Developers

The current main developers of Ultimate are:

Daniel Dietsch
Dominik Klumpp
Frank Schüssele
Matthias Heizmann

Most Ultimate developers are students and researchers in the software engineering group of Andreas Podelski at the University of Freiburg. Current and former developers of Ultimate are

Alexander Nutz
Alex Saukh (web interface, CDT interface, CACSL2Boogie, Büchi minimization)
Arend v. Reinersdorff (predecessor of Ultimate)
Bat-Chen Golden (incremental verification)
Ben Biesenbach (predicate trie, underapproximating loop acceleration)
Betim Musa (automata script, interpolants from unsatisfiable cores, incremental proof generation, interpolant consolidation, invariant synthesis)
Björn Buchhold (predecessor of Ultimate, the 2.0 version)
Björn Hagemeister (DFA minimization)
Claus Schätzle (procedure inlining, abstract interpretation octagon domain, Petri nets, SIFA)
Chen Kefei (nested interpolants)
Christian Ortolf (predecessor of Ultimate)
Christian Schilling
Christian Simon (predecessor of Ultimate, the 2.0 version)
Christoph Hofmann (Ultimate in the cloud)
David Zschocke (invariant synthesis)
Daniel Christiany (NWA)
Daniel Küchler (Büchi Petri nets)
Daniel Tischner (random automata, DFA minimization, Büchi minimization, NWA minimization)
Daniel Wadehn (delta debugger)
Dennis Wöfling (danger invariants, repeated Lipton reduction, maximal causality reduction)
Dirk Steinmetz (invariant synthesis)
Dominik Nuber (floating point)
Elisabeth Henkel (MSO solver)
Elisabeth Schanno (Lipton reduction)
Evren Ermis
Fabian Reiter (Büchi complementation)
German Fordinal (Webinterface)
Guilherme Schievelbein (floating point)
Jacob Maxam (counting automata)
Jan Leike (NWA, LassoRanker)
Jan Hättig (total interpolation, abstract interpretation polyhedra domain)
Jan Mortensen (NWA, Petri nets)
Jan Oreans (invariant synthesis)
Jeffery Hsu (incremental inclusion)
Jens Stimpfle (NWA minimization)
Jelena Barth (Jung visualization)
Jeremi Dzienian (Temporal Properties)
Jochen Hoenicke
Johannes Wahl (Concurrent Abstract Interpretation)
Jonas Werner (Loop Acceleration with Abstracting Path Conditions, PDR, Accelerated Interpolation for Trace Abstraction)
Julian Jarecki (Petri nets)
Julian Löffler (Heuristic Search for Counterexamples)
Jürgen Christ
Justus Bisser (predecessor of Ultimate)
Lars Nitzke (pthreads)
Layla Franke (DFA minimization)
Leonard Fichtner (polynomial terms)
Marc Fuchs (multi-step automata)
Marcel Ebbinghaus (counting automata, sleep set reduction)
Marcel Rogg (POR statement abstraction)
Markus Lindenmann (web interface, CDT interface, CACSL2Boogie, Büchi minimization, C memory model)
Markus Pomrehn (formula simplification, alternating automata)
Markus Zeiger (NWA, E-Matching)
Marius Greitschus
Matthias Keil (Prefuse visualization)
Max Barth (quantifier elimination, bitvector-integer translation)
Maximilian Rohland (floating point)
Mehdi Naouar (Petri nets)
Miriam Herzig (Jordan Loop Acceleration)
Miriam Lagunes (Owicki-Gries annotations)
Moritz Mohr (Loop Acceleration with Abstracting Path Conditions)
Nico Hauff (MSO solver, ReqChecker, Build System)
Nicola Sheldrick (predecessor of Ultimate)
Numair Mansur (fault localization)
Robert Jakob (predecessor of Ultimate)
Saskia Rabald (multi-step automata)
Simon Ley (IC3)
Stefan Wissert (Web interface, CDT interface, CACSL2Boogie, IValuations, large block encoding)
Thomas Lang (loop complexity, bitvectors)
Tilo Heep (DPOR)
Tobias Grugel (tree automata)
Vincent Langenfeld
Xiaolin Wu (Büchi NWA emptiness check, Büchi NWA complementation)
Yu-Wen Chen (alias analysis)