Martin Bromberger
Doctoral researcher for
Arithmetic Reasoning
Max-Planck-Institut für Informatik
Campus E1 4
66123 Saarbrücken
+49 681 9325-2922, fax -2999
Physical address: building E1 5, room 634
Personal Information
Research Interests
- (Linear) Arithmetic Decision Procedures
- Theorem Proving
- Combination of Theories
- Parsing
Academic Activities
Teaching
- Tutor for Programmierung 1 WS 2010 by Prof. Dr. Gert Smolka
Recent Positions
- October 2011 - July 2014:
Hiwi for the Research Group 1: Automation of Logic at the Max-Planck-Institut für Informatik
Education
- July 2014 - present:
PhD student in Computer Science at the Universität des Saarlandes, Saarbrücken, Germany and the Max-Planck-Institut für Informatik - October 2012 - July 2014:
Student in the preparatory phase of the Graduate School of Computer Science at Universität des Saarlandes, Saarbrücken, Germany - October 2009 - March 2016:
Bachelor and Master student in Computer Science at the Universität des Saarlandes, Saarbrücken, Germany
Oct. 2010: BSc in Computer Science; thesis title: Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic (supervisor: Prof. Dr. Christoph Weidenbach)
Mar. 2016: MSc in Computer Science; thesis title: Analysis and Implementation of LIA Solvers: CutSAT and BBSAT (supervisor: Prof. Dr. Christoph Weidenbach)
Software Projects
SPASS
Wrote the parser for SPASS version 3.9SPASS-IQ
Main developer of the linear arithmetic theory solver SPASS-IQSPASS-SATT
Main developer of the CDCL(LA) solver SPASS-SATTAwards:
SMT-COMP 2018 (13th International Satisfiability Modulo Theories Competition)- First Place in the main track in the QF_LIA division
- Best Newcomer Award
- First Place in the single query track in the QF_LRA (Seq.) division
Publications
- SPASS-SATT a CDCL(LA) Solver, Martin Bromberger, Mathias Fleury, Simon Schwarz, and Christoph Weidenbach. In CADE-27, volume 11716 of LNCS, pages 111–122. Springer, 2015. Springer Link version (PDF, HTML); (***Best Student Paper Award***)
- A Complete and Terminating Approach to Linear Integer Solving, Martin Bromberger, Thomas Sturm, and Christoph Weidenbach. Accepted for publication in the SC-Square Special Issue of the Journal of Symbolic Computation (JSC). ScienceDirect online version (PDF);
- A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems, Martin Bromberger. IJCAR 2018, volume 10900 of LNCS, pages 329–345. Springer, 2018. Springer Link version (PDF, HTML); extended arXiv version (PDF);
- New Techniques for Linear Arithmetic: Cubes and Equalities, Martin Bromberger, and Christoph Weidenbach. In FMSD volume 51(3), pages 433–461. Springer, 2017. Springer Link version (PDF, HTML, Open access);
- Computing a Complete Basis for Equalities Implied by a System of LRA Constraints, Martin Bromberger, and Christoph Weidenbach. In SMT@IJCAR, volume 1617 of CEUR Workshop Proceedings, pages 15–30. CEUR-WS.org, 2016. CEUR-WS version (PDF, Open access);
- Fast Cube Tests for LIA Constraint Solving, Martin Bromberger, and Christoph Weidenbach. In IJCAR 2016, volume 9706 of LNCS, pages 116–132. Springer, 2016. Author's version (PDF); Springer Link version (PDF, HTML);
- Linear Integer Arithmetic Revisited,Martin Bromberger, Thomas Sturm, and Christoph Weidenbach. In CADE-25, volume 9195 of LNCS, pages 623–637. Springer, 2015. Springer Link version (PDF, HTML); extended arXiv version (PDF);