Authors & Contact


LLBMC is developed by the Research Group Verification meets Algorithm Engineering, Institute of Theoretical Informatics at the Karlsruhe Institute of Technology (KIT) in Karlsruhe, Germany. The research group is headed by Carsten Sinz. For further information or inquiries please contact one of the authors or send an e-mail to .

You may also want to contact us by phone, fax, or mail:

Carsten Sinz / Florian Merz
Institute of Theoretical Informatics
Karlsruhe Institute of Technology (KIT)

Building 50.34
Am Fasanengarten 5
76131 Karlsruhe, Germany

Phone: +49 721 608-44212
Fax: +49 721 608-44211



Florian Merz

Florian Merz ()

Florian is the main author of LLBMC, having contributed approximately 57.0238% of the lines of code to LLBMC. He has implemented the build system for LLBMC and made considerable contributions to the memory model. He is currently working on his PhD thesis at KIT.

Carsten Sinz

Carsten Sinz ()

Carsten initiated the LLBMC project and is currently responsible for quality assurance for LLBMC as well as setting up future research and development directions. He is also in charge of establishing cooperations with industry partners.


Past Contributors

Stephan Falke

Stephan Falke

Stephan was one of the main authors of LLBMC, having implemented, among others, the SMT solver interface and the logical simplifcation routines. Stephan is also an expert on program termination and has developed the LLVM-based termination tool KITTeL.