Martin Bromberger
Dr. Martin Bromberger
Senior researcher for
Combinations of Theories and 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 - December 2019:
PhD student in Computer Science at the Universität des Saarlandes, Saarbrücken, Germany and the Max-Planck-Institut für Informatik
December 2019: finished PhD in Computer Science (Dr. rer. nat.); thesis title: Decision Procedures for Linear Arithmetic - 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: finished BSc in Computer Science; thesis title: Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic (supervisor: Prof. Dr. Christoph Weidenbach)
Mar. 2016: finished 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
- A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic, Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Larry González, Markus Krötzsch, Maximilian Marx, Harish K. Murali, Christoph Weidenbach. To appear in the proceedings of TACAS 2022. Springer, 2022. Author's version (PDF);
- A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic, Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer, Markus Krötzsch, Christoph Weidenbach. In FroCoS 2021, volume 12941 of LNCS, pages 3–24. Springer, 2021.
- Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories, Martin Bromberger, Alberto Fiori, and Christoph Weidenbach. In VMCAI 2021, volume 12597 of LNCS, pages 511–533. Springer, 2021. Author's version (PDF); Springer Link version (PDF, HTML);
- Decision Procedures for Linear Arithmetic, Martin Bromberger. PhD thesis (submitted in July 2019, defended in December 2019).
DOI: 10.22028/D291-30636; PDF version; (***Dr.-Eduard-Martin-Preis***)
- 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);